leanprover-community / repl

A simple REPL for Lean 4, returning information about errors and sorries.
54 stars 13 forks source link

Repl doesn't return any output? #16

Open Kreijstal opened 8 months ago

Kreijstal commented 8 months ago

I am trying to use the repl, I have no idea how is it supposed to work but I receive no output

> lake exe repl
{ "cmd" : "def f := 2" }
{ "cmd" : "example : f = 2 := rfl", "env" : 1 }
{ "cmd" : "#eval 1+1"} 
{ "cmd" : "IO.println \"hey\""} 

after ctr+c I get

uncaught exception: {"message": "offset 34: expected end of input"}

am I doing something wrong?

digama0 commented 8 months ago

I had to insert two newlines between each command (or press enter twice after each line) to receive a response. If you only use one newline you get the expected end of input error message.

Kreijstal commented 8 months ago

meanwhile in my machine

> lake exe repl
{ "cmd" : "#eval 1+1"}

\r\n

(doesn't seem to work)

digama0 commented 8 months ago

what OS and terminal are you using? Most terminals submit the result after each line. Ctrl-D should work to close the input stream and push everything, but it's obviously not optimal since you can't write anything after that.

digama0 commented 8 months ago

It seems like this code:

/-- Get lines from stdin until a blank line is entered. -/
partial def getLines : IO String := do
  match (← (← IO.getStdin).getLine) with
  | "" => pure ""
  | "\n" => pure "\n"
  | line => pure <| line ++ (← getLines)

may fail on windows and cause it to keep asking for lines forever if a blank line is sent as "\r\n" rather than "\n". cc: @semorrison

Kreijstal commented 8 months ago

I am using vscode under windows

semorrison commented 8 months ago

@Kreijstal, would you mind checking if the problem has been resolved now?