working with the lean4 repository in VSCode

Stream: lean4

[Scott Morrison]

It seems that at the moment if you just open the lean4 repository in VSCode (with the lean4 extension) and open one of the .lean files, it doesn't interactively compile. To get it to work I have to use elan override set (either to a local toolchain where I've compiled from source, or a nightly toolchain).

This is just because without an override, elan may be providing the stable version of lean3 as the default server!

Presumably this is only a temporary situation until there is a lakefile.lean for lean4 itself?

Whether or not it is temporary, should we add a line in the manual about needing to use elan override? (If this is the correct thing to do, I can do it.)

[Gabriel Ebner]

This has always been the case, also in Lean 3. I believe the elan setup is even explicitly documented here: https://leanprover.github.io/lean4/doc/dev/index.html?highlight=elan#dev-setup-using-elan

[Gabriel Ebner]

I don't think we can automate the elan override set part, because it's not always clear which build you want (i.e., build/release/stage0 or build/release/stage1). But setting LEAN_SRC_PATH automatically should be feasible though.

[Sebastian Ullrich]

What Gabriel said. LEAN_SRC_PATH is set automatically when using nix-shell https://github.com/leanprover/lean4/blob/3546104959f6048adfcbde5e72a1ca98abf03e6f/shell.nix#L20

[Scott Morrison]

Sorry, you're absolutely right. Perhaps it would be helpful to rearrange a little so this advice comes before the actual build-from-source instructions, as it is potentially relevant if you don't want to touch any of the C code, but just edit one .lean file. But low priority.