diff --git a/Main.lean b/Main.lean index bed33bb..59a7e95 100644 --- a/Main.lean +++ b/Main.lean @@ -22,7 +22,7 @@ def parseCommand (s: String): Except String Protocol.Command := do return { cmd := s.take offset, payload := payload } | .none => throw "Command is empty" -unsafe def loop : MainM Unit := do +partial def loop : MainM Unit := do let state ← get let command ← (← IO.getStdin).getLine if command.trim.length = 0 then return () diff --git a/Test/Main.lean b/Test/Main.lean index cb7c055..82d8748 100644 --- a/Test/Main.lean +++ b/Test/Main.lean @@ -6,8 +6,7 @@ import Test.Serial open Pantograph.Test -unsafe def main := do - Lean.enableInitializersExecution +def main := do Lean.initSearchPath (← Lean.findSysroot) let suites := [