Wrong version in VS Code

Stream: lean4

[Arthur Paulino]

Hi! I am updating my toolchain to leanprover/lean4:nightly-2022-10-06. After the code fixes, I am now able to run lake build. But, in VS Code, it's behaving as if I were still using the previous version (leanprover/lean4:nightly-2022-07-11). So the code compiles via terminal but it's completely broken in VS Code. Has anyone seen anything similar?

[Jeremy Avigad]

It sounds vaguely familiar but if I have seen it before I don't remember what I did. Maybe try elan show in the terminal to see if there are any overrides?

[Arthur Paulino]

λ elan show
installed toolchains
--------------------

stable
leanprover/lean4:nightly
leanprover/lean4:nightly-2022-07-11 (default)
leanprover/lean4:nightly-2022-07-16
leanprover/lean4:nightly-2022-09-11
leanprover/lean4:nightly-2022-10-06

active toolchain
----------------

leanprover/lean4:nightly-2022-10-06 (overridden by '/home/arthur/dev/lean/viper/lean-toolchain')
Lean (version 4.0.0-nightly-2022-10-06, commit b172ba8a34e7, Release)

[Arthur Paulino]

Apparently it's picking that "default" toolchain. How can I make it pick the toolchain defined in my lean-toolchain file?

[Jeremy Avigad]

Check elan override help. Maybe elan override unset?

[Arthur Paulino]

λ elan override unset
info: no override toolchain for '/home/arthur/dev/lean/viper'
info: you may use `--path <path>` option to remove override toolchain for a specific path

[Jeremy Avigad]

I think I am out of ideas. It is strange that elan show says overridden but then elan override unset disagrees. But I really don't understand why using the command line in the root folder would yield a different result than VS Code.

[Gabriel Ebner]

"override" here just means that it picks up the version from the lean-toolchain file

[Gabriel Ebner]

@Arthur Paulino Have you restarted VS Code?

[Jeremy Avigad]

Also, sometimes deleting the build directory helps.

[Arthur Paulino]

Yes, I have restarted VS Code. I have also deleted the build folder

[Gabriel Ebner]

Another thing to try: run the "select toolchain" command, click "other", and then press enter. See also https://github.com/leanprover/vscode-lean4/issues/79

[Arthur Paulino]

#eval Lean.versionString or something still returns the old one

[Arthur Paulino]

Hmmm, I will try that solution tomorrow. Thanks!

[Arthur Paulino]

How to run that select toolchain command tho?

[Gabriel Ebner]

ctrl-shift-p

[Chris Lovett]

Just put "leanprover/lean4:nightly-2022-10-06" in your lean-toolchain file.

[Arthur Paulino]

@Chris Lovett that's what I have

[Chris Lovett]

I'm not able to reproduce this using the lean4-samples/HelloWorld. Can you?

[James Gallicchio]

I think recently I had to kill all the lean processes on my computer for vscode to switch over... It seems occasionally brittle to version updates

[Chris Lovett]

Wait, I think I have a repro, I installed leanprover/lean4:nightly-2022-10-06 specifically, and it is having trouble using it even after restarting VS code. So I'm investigating.

[Chris Lovett]

Interesting, I have changed the lean4-samples\HelloWorld\lean-toolchain to leanprover/lean4:nightly-2022-10-06 and got this:

(leanink) D:\git\leanprover\lean4-samples\HelloWorld>lake --version
Lake version 4.0.0 (Lean version 4.0.0-nightly-2022-09-26)

Turns out I didn't realize but I did have an elan override set in this folder:

(leanink) D:\git\leanprover\lean4-samples\HelloWorld>elan override list
D:\git\leanprover\lean4-samples\HelloWorld      leanprover/lean4:nightly-2022-09-26

So after removing that with elan override unset then VS code started working properly (after a Lean4: Restart Server).

[Chris Lovett]

so can you check your elan override list ?

[Sebastian Ullrich]

@Chris Lovett
Arthur Paulino said:

λ elan override unset
info: no override toolchain for '/home/arthur/dev/lean/viper'
info: you may use `--path <path>` option to remove override toolchain for a specific path

[Sebastian Ullrich]

I can think of only two further causes:

• You do not have the viper folder opened as the workspace folder
• Some Lean override local to VS Code, e.g. in its extension settings

[Arthur Paulino]

The solution was using Gabriel's idea with the "Select Lean toolchain" command (via ctrl-shift-p) and then choosing the option "Reset toolchain override" or something. Thanks everyone!

[Chris Lovett]

Yes when you use "Lean4: Select Toolchain" the selection you make is sticky for that folder, so to remove it you do have to use the "Reset workspace override". The "Lean4: Select Toolchain" command will show you when a workspace override is in effect:
image.png