aniva
/
Pantograph
1
1
Fork 0
Code Issues 6 Pull Requests 2 Packages Projects Releases 1 Wiki Activity

Fix test failures

pull/28/head
Leni Aniva 2023-10-05 17:51:41 -07:00
parent a8cf94ccb1
commit 13f3460e9a
3 changed files with 3 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Test/Integration.lean
View File

@ -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 := {

2
Test/Proofs.lean
View File

@ -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 := [

2
Test/Serial.lean
View File

@ -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)