Merge branch 'dev' into goal/continuation

This commit is contained in:
Leni Aniva 2023-11-06 11:45:24 -08:00
commit 32fedede6a
2 changed files with 2 additions and 3 deletions

View File

@ -22,7 +22,7 @@ def parseCommand (s: String): Except String Protocol.Command := do
return { cmd := s.take offset, payload := payload } return { cmd := s.take offset, payload := payload }
| .none => throw "Command is empty" | .none => throw "Command is empty"
unsafe def loop : MainM Unit := do partial def loop : MainM Unit := do
let state ← get let state ← get
let command ← (← IO.getStdin).getLine let command ← (← IO.getStdin).getLine
if command.trim.length = 0 then return () if command.trim.length = 0 then return ()

View File

@ -6,8 +6,7 @@ import Test.Serial
open Pantograph.Test open Pantograph.Test
unsafe def main := do def main := do
Lean.enableInitializersExecution
Lean.initSearchPath (← Lean.findSysroot) Lean.initSearchPath (← Lean.findSysroot)
let suites := [ let suites := [