Zulip Chat Archive

Stream: lean4

Topic: can't print unit


view this post on Zulip Mario Carneiro (Apr 12 2021 at 05:19):

This crashes the lean server:

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

view this post on Zulip Mario Carneiro (Apr 12 2021 at 05:27):

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

view this post on Zulip Mario Carneiro (Apr 12 2021 at 05:28):

since this also fails

#eval IO.print ""

view this post on Zulip Mario Carneiro (Apr 12 2021 at 05:35):

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

#eval show TermElabM String from throwError "foo"

view this post on Zulip Sebastian Ullrich (Apr 12 2021 at 09:44):

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.

view this post on Zulip Mario Carneiro (Apr 12 2021 at 10:18):

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

view this post on Zulip Mario Carneiro (Apr 12 2021 at 10:18):

in vscode

view this post on Zulip Mario Carneiro (Apr 12 2021 at 10:18):

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

view this post on Zulip Sebastian Ullrich (Apr 12 2021 at 10:18):

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


Last updated: May 07 2021 at 12:15 UTC