From 13f3460e9a5b5666b6d9c1a150b659da9e958e77 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Thu, 5 Oct 2023 17:51:41 -0700
Subject: [PATCH] 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)