Zulip Chat Archive

Stream: lean4

Topic: making lean and lean4 coexist


Alice Laroche (Feb 03 2022 at 21:26):

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 (Feb 03 2022 at 21:28):

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

Alice Laroche (Feb 03 2022 at 21:31):

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 (Feb 03 2022 at 21:39):

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 (Feb 03 2022 at 21:46):

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

Marc Huisinga (Feb 03 2022 at 21:48):

Are you running Windows by any chance?

Alice Laroche (Feb 03 2022 at 21:50):

Nop, brrr, this is good ol' arch

Arthur Paulino (Feb 03 2022 at 21:51):

Which version of the Lean 4 extension are you using?

Alice Laroche (Feb 03 2022 at 21:51):

last one, 0.63

Mac (Feb 03 2022 at 22:01):

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

Mario Carneiro (Feb 03 2022 at 22:08):

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

Mario Carneiro (Feb 03 2022 at 22:09):

I think they are currently indistinguishable

Alice Laroche (Feb 03 2022 at 22:10):

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

Marc Huisinga (Feb 03 2022 at 22:14):

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 (Feb 03 2022 at 22:17):

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

Marc Huisinga (Feb 03 2022 at 22:19):

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 (Feb 04 2022 at 12:04):

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 (Feb 04 2022 at 12:06):

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 (Feb 04 2022 at 12:41):

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 (Feb 04 2022 at 12:43):

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 (Feb 04 2022 at 12:44):

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 (Feb 04 2022 at 13:01):

That's what I meant as well.

Marc Huisinga (Feb 04 2022 at 16:28):

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 (Feb 08 2022 at 03:27):

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 (Feb 08 2022 at 03:59):

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 (Feb 08 2022 at 05:43):

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 (Feb 08 2022 at 08:19):

Chris Lovett said:

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

We have no such file, do we?

Sebastian Ullrich (Feb 08 2022 at 08:20):

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 (Feb 08 2022 at 08:59):

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 (Feb 08 2022 at 10:30):

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).


Last updated: Dec 20 2023 at 11:08 UTC