Better support for old Lean

leanprover · Aug 9, 2024 · fd30933 · fd30933
1 parent 23583f8
commit fd30933
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 1 deletion.
diff --git a/Extract.lean b/Extract.lean
@@ -3,6 +3,7 @@ Copyright (c) 2023-2024 Lean FRO LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: David Thrane Christiansen
 -/
+import SubVerso.Compat
 import SubVerso.Examples.Env
 
 open Lean
@@ -13,7 +14,7 @@ def main : (args : List String) → IO UInt32
     try
       initSearchPath (← findSysroot)
       let modName := mod.toName
-      let env ← importModules #[{module := modName, runtimeOnly := false}] {}
+      let env ← SubVerso.Compat.importModules #[{module := modName, runtimeOnly := false}] {}
       let modExamples := highlighted.getState env
       let useful := relevant modName modExamples
       let exJson := Json.mkObj useful

diff --git a/src/compat/SubVerso/Compat.lean b/src/compat/SubVerso/Compat.lean
@@ -49,6 +49,9 @@ open Command in
 elab "%if_bound" x:ident cmd:command : command => do
   if (← getEnv).contains x.getId then elabCommand cmd
 
+def importModules (imports : Array Import) (opts : Options) (trustLevel : UInt32 := 0) : IO Environment :=
+  Lean.importModules (%first_succeeding [imports, imports.toList]) opts (trustLevel := trustLevel)
+
 def mkRefIdentFVar [Monad m] [MonadEnv m] (id : FVarId) : m Lean.Lsp.RefIdent := do
   pure %first_succeeding [
     .fvar (← getEnv).mainModule id,