Skip to content

Commit

Permalink
avoid buffering stdout to ensure immediate replies (#49)
Browse files Browse the repository at this point in the history
  • Loading branch information
m4lvin authored Jul 26, 2024
1 parent ff1baf8 commit 4fc1e6d
Showing 1 changed file with 7 additions and 1 deletion.
8 changes: 7 additions & 1 deletion REPL/Main.lean
Original file line number Diff line number Diff line change
Expand Up @@ -302,6 +302,12 @@ def parse (query : String) : IO Input := do
| .error e => throw <| IO.userError <| toString <| toJson <|
(⟨"Could not parse as a valid JSON command:\n" ++ e⟩ : Error)

/-- Avoid buffering the output. -/
def printFlush [ToString α] (s : α) : IO Unit := do
let out ← IO.getStdout
out.putStr (toString s)
out.flush -- Flush the output

/-- Read-eval-print loop for Lean. -/
unsafe def repl : IO Unit :=
StateT.run' loop {}
Expand All @@ -318,7 +324,7 @@ where loop : M IO Unit := do
| .unpickleEnvironment r => return toJson (← unpickleCommandSnapshot r)
| .pickleProofSnapshot r => return toJson (← pickleProofSnapshot r)
| .unpickleProofSnapshot r => return toJson (← unpickleProofSnapshot r)
IO.println "" -- easier to parse the output if there are blank lines
printFlush "\n" -- easier to parse the output if there are blank lines
loop

/-- Main executable function, run as `lake exe repl`. -/
Expand Down

0 comments on commit 4fc1e6d

Please sign in to comment.