Multiple versions of lean in one vscode session

Stream: lean4

[Mario Carneiro]

I thought that this was impossible, but today I saw something unusual and now I'm not sure I understand the system.

To summarize my setup, I have a project lean4-test in which there is a elan override set lean4-stage1 which points to the stage1 dev build of lean4, which I use for testing lean4 changes in a standalone lake project. Currently I open this in a separate vscode instance from the one I use for the lean4 repo itself. This was not entirely by choice, I originally tried opening the test files from the same instance but they get built using stage0 when you do that so it isn't suitable for testing. Having a separate vscode instance means that it uses stage1 in the lean4-test folder and all is well.

Now, sometimes I want to open a file inside lean4/tests. As mentioned I can't do that from the lean4 vscode instance directly, but I can drag those files to the lean4-test instance to check them using stage1, because as I mentioned vscode uses the version of lean set at the project root for everything opened in that vscode instance. However, today I tried to do that and it did not work: the server seems to be using stage0 for files in the tests folder and stage1 in the lean4-test folder, from the lean4-test instance, which I thought was impossible. Did lake serve change the way it resolves which lean to call?

If I do #eval Lean.versionString from lean4/tests/lean/run/foo.lean I get "4.0.0, commit ", and #eval Lean.versionString from lean4-test/Test.lean I get "4.0.0, commit 45b3c4eabe5c11a904f64535e25ca88d892da893", although both link to the same source file from lean4 directory. I don't know a good way to ascertain whether I am actually looking at stage0 and stage1 here, but that would make the most sense.

[Wojciech Nawrocki]

Not quite an answer to your question, but if you open multiple folders in one VSCode workspace they should use their respective version of Lean. This includes opening a subfolder, e.g. if you have the Lean 4 dev setup and a workspace with both lean4 and lean4/src open as folders, the latter will use stage0 whereas the former will use stage1.

[Mario Carneiro]

I'm not using a multiple-folder workspace. I have lean4-stage0 set in lean4 root and lean4-stage1 set in lean4/tests, and my observation is that from the lean4 project opening files in tests still uses stage0, but if I open tests as a folder on its own then it uses stage1

[Mario Carneiro]

but opening lean4/tests from lean4-test (which is a completely separate folder which also has a lean4-stage1 override) uses stage0, which I can't make any sense of

[Mario Carneiro]

where is the logic for this implemented?

[Wojciech Nawrocki]

What is lean4-test?

[Mario Carneiro]

it's a separate project outside the lean4 directory

[Mario Carneiro]

it's a basic hello world lake project

[Wojciech Nawrocki]

If you have a stage1 override there and you use that as your vsc workspace root, it should use stage1.

[Mario Carneiro]

It does, inside the folder itself

[Wojciech Nawrocki]

I don't know what you mean by "opening lean4/tests from lean4-test". Did you use Add folder to workspace? Then that's a multi-folder workspace.

[Mario Carneiro]

no, I mean opening a file outside the folder

[Mario Carneiro]

i.e. "open file" and navigate outside the folder, or drag a file from another vscode instance to it

[Wojciech Nawrocki]

Oh, you had lean4-test as the workspace root and then opened a standalone file in lean4/tests ?

[Mario Carneiro]

yes

[Wojciech Nawrocki]

Ah I see, there might be some logic in vsc or vsc-lean4 that essentially treats that as if it were its own root in the workspace.

[Mario Carneiro]

my experience has been that this will still use stage1 regardless of any overrides in lean4 or lean4/tests

[Mario Carneiro]

but today it used stage0 and I don't know why

[Wojciech Nawrocki]

Vsc 1.79 was released two hours ago, possible that the logic changed.

[Mario Carneiro]

I'm not using it yet

[Mac Malone]

@Mario Carneiro Could it be that instead of using stage0/stage1, it is actually using the default toolchain in elan and that may have changed?

[Mario Carneiro]

do you know how I can determine the version more precisely?

[Mario Carneiro]

maybe get the olean root

[Mario Carneiro]

aha, #eval IO.appDir returns stage0/bin indeed

[Mario Carneiro]

@Mac there are overrides everywhere, I don't see how it could be using the default toolchain

[Mac Malone]

VS Code runs toolchain binaries directly, not through elan. So, if it some gets a bad setup it can circumvent overrides.

[Mario Carneiro]

Mario Carneiro said:

where is the logic for this implemented?

[Mario Carneiro]

I don't really understand how work is distributed among lake serve, lean --server and the vscode extension

[Mac Malone]

Right now, lake serve is essentially just sugar for lake env lean --server <extra user args...>

[Mac Malone]

VS Code either use its settings for the Lean toolchain path and Lake path or the system version (i.e., whatever lean and lake in path are).

[Mario Carneiro]

FWIW the "lean4.toolchainPath" setting is unset in lean4-test in this situation

[Mario Carneiro]

Okay so poking around in the output of ps reveals that

/home/mario/Documents/lean/lean4/build/release/stage0/bin/lean --worker file:///home/mario/Documents/lean/lean4/tests/lean/run/cdotTests.lean

was started by

/home/mario/.elan/toolchains/lean4-stage0/bin/lean --server /home/mario/Documents/lean/lean4

which was started by code, which suggests that elan and/or the vscode configuration is at fault somehow

[Mario Carneiro]

apparently the code process for lean4-test has two lean --server children:

/home/mario/.elan/toolchains/lean4/bin/lean --server /home/mario/Documents/lean/lean4-test
/home/mario/.elan/toolchains/lean4-stage0/bin/lean --server /home/mario/Documents/lean/lean4

I guess I need to read the extension code because this shouldn't be possible

[Mac Malone]

If you open a file outside of a project, my understanding is that kind of works like new special single-file project (in the same way an untitled file does).

[Mario Carneiro]

Mario Carneiro said:

where is the logic for this implemented?

[Mario Carneiro]

hm, you might be on to something, I tried opening lean4/tests/lean/run/cdotTests.lean in a standalone vscode instance (no "open folder") and it used stage0

[Mario Carneiro]

despite the fact that elan show in the containing directory tells me that the active toolchain is lean4-stage1

[Mac Malone]

What are the VS Code settings for Lean toolchain and Lake Path when you open the file standalone?

[Mario Carneiro]

there are no custom settings at all

[Mario Carneiro]

both of those are set to the empty string

[Mario Carneiro]

having read leanclient.ts I'm now sure I don't understand. The command line invocation above clearly shows that the cwd for the lean --server invocation is /home/mario/Documents/lean/lean4 but the code never sets cwd when folderUri is null (which I guess is the case when opening a standalone file?), and the cwd of the code process itself is just /home/mario so I have no idea what gave it the idea to look at the lean4 directory and not one of its parents or children. My only theory is that there happens to be a git directory there