Zulip Chat Archive

Stream: lean4

Topic: VS Code

Heather Macbeth (Dec 08 2022 at 12:53):

Is this the right stream for questions about the Lean 4 VS Code extension? Two things I have noticed:

  • when I run "Lean: Restart" (via cmd-shift-p), which was a standard part of my toolkit in Lean 3, I get Command 'Lean: Restart' resulted in an error (command 'lean.restartServer' not found). Is something not hooked up, or does this have a different name in Lean 4?
  • when I comment out an import line, the keyword import remains blue even as the rest of the line turns green.

I can open issues for these at https://github.com/leanprover/vscode-lean4, but first wanted to check whether they were actually considered issues.

Kevin Buzzard (Dec 08 2022 at 13:01):

Lean: restart is for Lean 3 -- there's a Lean4 restart.

Heather Macbeth (Dec 08 2022 at 13:11):

Ok great! One down.

Trebor Huang (Dec 08 2022 at 16:04):

You can check why the highlight works that way by the command "Developer: Inspect Tokens and something I forgot" to see if it is intended.

Last updated: Dec 20 2023 at 11:08 UTC