making lean and lean4 coexist

Stream: lean4

[Alice Laroche]

So... it's embarrising.
I tried to tweak some configuration in VS Code and now the lean extension try to run even if i'm in a lean4 folder, and i can't run lean4.restartServer

[Alex J. Best]

You can disable extensions for a given workspace by right clicking them in the extensions bar

[Alice Laroche]

Well it work... kinda.
Before i didn't had to disactivate extensions. And for some reason,i don't have infoview in Lean sources anymore

[Arthur Paulino]

I managed to make it work by allowing the Lean 4 extension to pop in every Lean project, except for mathlib (the only Lean 3 project I tweak). And the Lean 3 extension is restricted to mathlib

[Alice Laroche]

Hmm, Lean 4 is enabled globaly tho
Like, why nothing show up in the infoview
image.png

[Marc Huisinga]

Are you running Windows by any chance?

[Alice Laroche]

Nop, brrr, this is good ol' arch

[Arthur Paulino]

Which version of the Lean 4 extension are you using?

[Alice Laroche]

last one, 0.63

[Mac]

My first thought: is that the Lean 3 extension infoview or the Lean 4 extension infoview?

[Mario Carneiro]

maybe they should have a different title bar so you can tell the difference

[Mario Carneiro]

I think they are currently indistinguishable

[Alice Laroche]

You can distinguish them by adding some different CSS to both
But it's not a great solution

[Marc Huisinga]

FWIW on the latest nightly and Lean 4 VSCode extension version, my editor doesn't seem to be responsive either (No diagnostics, no infoview contents, etc.). I tried both Windows and WSL and older nightlies where I think it used to work as well.

[Alice Laroche]

So what actually happend was , while I was tweaking configuration, the extension updated and change behavior... i guess ?

[Marc Huisinga]

Marc Huisinga said:

FWIW on the latest nightly and Lean 4 VSCode extension version, my editor doesn't seem to be responsive either (No diagnostics, no infoview contents, etc.). I tried both Windows and WSL and older nightlies where I think it used to work as well.

Ah, this may be related to me opening single files, not entire Lean projects?

[Gabriel Ebner]

Ah, this may be related to me opening single files, not entire Lean projects?

I didn't even know that vscode had such a mode. It's certainly completely untested.

[Gabriel Ebner]

is that the Lean 3 extension infoview or the Lean 4 extension infoview? [...] maybe they should have a different title bar so you can tell the difference

Yeah, it would be good to show some status info. Lean version in the status bar. And "server not running" or smth in the infoview instead of "no info found" and "no messages".

[Marc Huisinga]

Gabriel Ebner said:

Ah, this may be related to me opening single files, not entire Lean projects?

I didn't even know that vscode had such a mode. It's certainly completely untested.

Opening single Lean 4 files worked fine until a few updates ago (as long as you have some global Lean installation). The server has (had?) support for it as well, since I thought that creating a single file and running a bit of isolated Lean code is neat for testing things, similar to how you'd just launch up a REPL.

[Gabriel Ebner]

Did some limited testing right now. Create a file x/y.lean without lakefile. Then code x and opening y.lean works. But code x/y.lean doesn't. That's what I meant by special single-file mode.

[Gabriel Ebner]

Also the UI is very different. E.g. you don't get the usual modal trust dialog, but a notification that the extensions are disabled.

[Marc Huisinga]

That's what I meant as well.

[Marc Huisinga]

Hm, my extensions aren't disabled when I open a single new .lean file, but I don't seem to get the trust dialog either, which is strange

[Chris Lovett]

I have a fix in progress here with some questions about how you want this to behave: https://github.com/leanprover/vscode-lean4/pull/117

[Julian Berman]

lean.nvim does the stdlib path walking you mention (actually just it looks for /lib/lean in the path) and I think it works pretty well.

[Chris Lovett]

Right my question is if you open leanprover--lean4---nightly\lib\lean\src\Init\System\IO.lean do you expect it to find and use leanprover--lean4---nightly\lib\lean\src\leanpkg.toml or an inherited lean-toolchain in the case of something like mathlib. Specifically it would start a lean --server in that folder so that any other files opened in that directory tree would also use the same lean --server. I think this is probably the right behavior, but I just wanted to check if this matches your expectation.

[Sebastian Ullrich]

Chris Lovett said:

leanprover--lean4---nightly\lib\lean\src\leanpkg.toml

We have no such file, do we?

[Sebastian Ullrich]

Julian Berman said:

lean.nvim does the stdlib path walking you mention (actually just it looks for /lib/lean in the path) and I think it works pretty well.

@Julian Berman Btw, note https://github.com/leanprover/lean4/pull/989

[Chris Lovett]

We have no such file, do we?

Woops you are right, I must have mistaken Leanpkg.lean for leanpkg.toml. But anyway, the same applies to mathlib4, if someone uses "file/open..." and opens mathlib4\Mathlib\Data\List\Basic.lean I assume the vscode extension should find the mathlib4\lean-toolchain file and start the lean --server in that folder, right?

[Gabriel Ebner]

I assume the vscode extension should find the mathlib4\lean-toolchain file and start the lean --server in that folder, right?

Right. For reference, the lean.nvim plugin looks for lean-toolchain, leanpkg.toml, and lakefile.lean files as well as the lib/lean directory (which will soon become src/lean).