Zulip Chat Archive

Stream: lean4

Topic: MetaM behaviour in vscode-lean4


view this post on Zulip Uranus Testing (Feb 02 2021 at 15:46):

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?

view this post on Zulip Sebastian Ullrich (Feb 02 2021 at 15:53):

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

view this post on Zulip Mario Carneiro (Feb 02 2021 at 16:02):

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

view this post on Zulip Marc Huisinga (Feb 02 2021 at 16:06):

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

view this post on Zulip Mario Carneiro (Feb 02 2021 at 16:08):

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

view this post on Zulip Marc Huisinga (Feb 02 2021 at 16:09):

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

view this post on Zulip Uranus Testing (Feb 06 2021 at 06:20):

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

view this post on Zulip Uranus Testing (Feb 06 2021 at 06:24):

And even in this version:

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

view this post on Zulip Uranus Testing (Feb 06 2021 at 06:37):

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

view this post on Zulip Sebastian Ullrich (Feb 06 2021 at 08:32):

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


Last updated: May 18 2021 at 22:15 UTC