From 836a14fa6396c7af6375b1bc9e4c653ed19ef5e3 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Thu, 5 Oct 2023 17:49:43 -0700
Subject: [PATCH 1/2] Bump Lean version to 4.1.0

---
 .gitignore     | 1 +
 Main.lean      | 2 +-
 lean-toolchain | 2 +-
 3 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/.gitignore b/.gitignore
index 069f8e2..21bcd46 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,5 +1,6 @@
 .*
 !.gitignore
 
+*.olean
 /build
 /lake-packages
diff --git a/Main.lean b/Main.lean
index dc4b14f..8fd617b 100644
--- a/Main.lean
+++ b/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 := {
diff --git a/lean-toolchain b/lean-toolchain
index 49fd71c..a9bddf0 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:4.0.0
+leanprover/lean4:4.1.0
-- 
2.44.1


From 5b002a9cebfef443141d798548224d709bbebb0d Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Thu, 5 Oct 2023 17:51:41 -0700
Subject: [PATCH 2/2] Fix test failures

---
 Test/Integration.lean | 2 +-
 Test/Proofs.lean      | 2 +-
 Test/Serial.lean      | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/Test/Integration.lean b/Test/Integration.lean
index ab31110..6caaf90 100644
--- a/Test/Integration.lean
+++ b/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 := {
diff --git a/Test/Proofs.lean b/Test/Proofs.lean
index ccf7b01..a6d08e7 100644
--- a/Test/Proofs.lean
+++ b/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 := [
diff --git a/Test/Serial.lean b/Test/Serial.lean
index e300492..058ba04 100644
--- a/Test/Serial.lean
+++ b/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)
 
-- 
2.44.1