can't print unit

Stream: lean4

[Mario Carneiro]

This crashes the lean server:

import Lean
open Lean Elab
#eval show TermElabM Unit from pure ()

[Mario Carneiro]

I think there is a bug in the server that causes it to crash when given an empty message

[Mario Carneiro]

since this also fails

#eval IO.print ""

[Mario Carneiro]

Not sure if this is related, but throwing also causes the server to crash

#eval show TermElabM String from throwError "foo"

[Sebastian Ullrich]

I can't reproduce any crashes. I can confirm that no messages are shown in the VS Code infoview if there is any empty/failing #eval, but not in Emacs.

[Mario Carneiro]

It's not a crash exactly, once #eval IO.print "" appears in the file the diagnostics stop getting updated

[Mario Carneiro]

in vscode

[Mario Carneiro]

there isn't any other indication that something has gone wrong, so it seems like the client is blocking forever on the request

[Sebastian Ullrich]

Yes, that I was able to reproduce. Seems to be a bug in the extension.