MetaM behaviour in vscode-lean4

Stream: lean4

[Uranus Testing]

import Lean.Meta
open Lean

#eval (throwError! "test" : MetaM Unit)
#eval 2 + 2

In the console it works properly:

$ lean metam-test.lean

metam-test.lean:4:0: error: test
4

But in VS Code only “processing...” appears on “#eval (throwError! …)” line. Is it OK?

[Sebastian Ullrich]

I can reproduce this in VS Code but not in Emacs, which is quite strange

[Mario Carneiro]

I noticed a similar behavior when I was playing with the int mod crash

[Marc Huisinga]

Maybe the file worker crashes and it displays the last diagnostic?

[Mario Carneiro]

is throwError! something explicitly in the monad or is this some runtime primitive?

[Marc Huisinga]

Okay no, the file worker doesn't actually crash, it just gets stuck

[Uranus Testing]

In the following snippet VSCode seems to get stuck too, when everything is fine in the console:

import Lean.Elab.Command
open Lean

syntax (name := hello) "hello" : command
@[commandElab «hello»] def elabHello : Elab.Command.CommandElab :=
λ stx => IO.println "hello!"

hello
#check 5

[Uranus Testing]

And even in this version:

@[commandElab «hello»] def elabHello : Elab.Command.CommandElab :=
λ stx => pure ()

[Uranus Testing]

After restarting “pure ()”-version becomes OK, but adding “IO.println” in elaborator breaks file checking every time.

[Sebastian Ullrich]

The language server communicates via stdout, so that's expected