.gitignore

@@ -1,5 +1,6 @@
 .*
 !.gitignore
 
+*.olean
 /build
 /lake-packages

Main.lean

@@ -88,7 +88,7 @@ unsafe def main (args: List String): IO Unit := do
   let imports:= args.filter (λ s => ¬ (s.startsWith "--"))
 
   let env ← Lean.importModules
-    (imports := imports.map (λ str => { module := str_to_name str, runtimeOnly := false }))
+    (imports := imports.toArray.map (λ str => { module := str_to_name str, runtimeOnly := false }))
     (opts := {})
     (trustLevel := 1)
   let context: Context := {

Test/Integration.lean

@@ -15,7 +15,7 @@ def subroutine_step (cmd: String) (payload: List (String × Lean.Json))
 def subroutine_runner (steps: List (MainM LSpec.TestSeq)): IO LSpec.TestSeq := do
   -- Setup the environment for execution
   let env ← Lean.importModules
-    (imports := [{module := Lean.Name.str .anonymous "Init", runtimeOnly := false }])
+    (imports := #[{module := Lean.Name.str .anonymous "Init", runtimeOnly := false }])
     (opts := {})
     (trustLevel := 1)
   let context: Context := {

Test/Proofs.lean

@@ -231,7 +231,7 @@ def proof_runner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq :
 
 def test_proofs : IO LSpec.TestSeq := do
   let env: Lean.Environment ← Lean.importModules
-    (imports := ["Init"].map (λ str => { module := str_to_name str, runtimeOnly := false }))
+    (imports := #["Init"].map (λ str => { module := str_to_name str, runtimeOnly := false }))
     (opts := {})
     (trustLevel := 1)
   let tests := [

Test/Serial.lean

@@ -64,7 +64,7 @@ def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do
 
 def test_serial: IO LSpec.TestSeq := do
   let env: Environment ← importModules
-    (imports := ["Init"].map (λ str => { module := str_to_name str, runtimeOnly := false }))
+    (imports := #["Init"].map (λ str => { module := str_to_name str, runtimeOnly := false }))
     (opts := {})
     (trustLevel := 1)
 

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:4.0.0
+leanprover/lean4:4.1.0