Elan override and VSCode extension

Stream: lean4 dev

[Joachim Breitner]

Following the documentation at https://lean-lang.org/lean4/doc/dev/index.html#dev-setup-using-elan I have set up lean overrides:

~/build/lean/lean4/src $ elan override list
/home/jojo/build/lean/lean4                 lean4-stage1
/home/jojo/build/lean/lean4/src             lean4-stage0
~/build/lean/lean4/src $ elan which lean
/home/jojo/.elan/toolchains/lean4-stage0/bin/lean

This used to work fine, but since a week or two, the VS code extension, when started in code src, complains

Opened folder is not a valid Lean 4 project folder because it does not contain a 'lean-toolchain' file. However, a valid Lean 4 project folder was found in one of the parent directories at '/home/jojo/build/lean/lean4'. Open this project instead?

and also

Cannot determine Lean version: no default toolchain

What should I do differently?

It helps to run

echo lean4-stage0 > ~/build/lean/lean4/src/lean-toolchain

but this seems wrong. Is it simply a infelicity of the VS code extension that it doesn’t take elan override into account?

[Marc Huisinga]

You can disable the message by unsetting Lean4: Show Invalid Project Warnings.

[Joachim Breitner]

But it’s not just the message, it says Waiting for Lean server to start... instead of starting lean, it seems.

[Marc Huisinga]

Does it go away after restarting the server?

[Joachim Breitner]

It does! Thanks

[Marc Huisinga]

Is it simply a infelicity of the VS code extension that it doesn’t take elan override into account?

Having some version of Lean available is unfortunately not sufficient to ensure that new users do not get stuck with broken setups. We need to ensure that they are in the right folder. The Lean 4 core directory is a bit of a special case, so there is a hack to detect it, but not for the src directory. I suppose I could add one for it as well :-)

[Joachim Breitner]

Either that, or simply document it at https://lean-lang.org/lean4/doc/dev/index.html#dev-setup-using-elan, either is fine with me.

[Joachim Breitner]

Although arguably if there is an elan override for a directory, then the user isn’t a new user and the code extension could just use that?

[Marc Huisinga]

I don't think we want to add any special handling for override, especially since Sebastian wants to get rid of it anyways

[Marc Huisinga]

... This made me notice vscode-lean4#351 though, which is good to fix regardless :)