From fd309332511aed89035fd8209456774888316b2d Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@davidchristiansen.dk>
Date: Fri, 9 Aug 2024 12:11:41 +0200
Subject: [PATCH] Better support for old Lean

---
 Extract.lean                    | 3 ++-
 src/compat/SubVerso/Compat.lean | 3 +++
 2 files changed, 5 insertions(+), 1 deletion(-)

diff --git a/Extract.lean b/Extract.lean
index 86d8c91..ec0eb75 100644
--- 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
index e35063d..14aa90c 100644
--- 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,