On the necessity of "open folder"

Stream: new members

[Mike Shulman]

I have been confused for weeks about why, when I open a Lean file in VS Code, it can't find any of its imports, even though there is a leanpkg.path file in the directory and Lean compiles the file just fine on the command line.

I just figured out, finally, that for some reason, when you "open a file" in VS Code, it invokes lean in some way that apparently prevents it from looking at the leanpkg.path file. In order for lean to behave normally in VS Code (i.e. the way it does on the command line), you have to first "open folder" and then click on the file you want to open inside the folder display.

This is extremely unintuitive for me. When I open a file in a text editor, I expect to be able to edit it in the same way regardless of how I happened to open it. Why does VS Code even have an "open file" option, if it doesn't open the file in a useful way? What exactly does this command do differently, and what is the use case for when someone would want that?

At least, it would be helpful to have some big red warnings about this in the Lean documentation. Now that I go back I see that the page on Lean projects indeed instructs me to use "Open folder"; but it doesn't give any indication that opening a file in this way is different from opening it with "Open file", so I naturally assumed that it didn't matter.

[Johan Commelin]

Even though I've been aware that I need to use "open folder" for 4 years, I have no idea what the underlying reason is. I would also like to know the answer to this question.

[Mario Carneiro]

VSCode has a notion of "workspaces" which are essentially defined by the folder that you open. The server is run from that directory, and it looks for leanpkg.path in that directory and its parents

[Mario Carneiro]

if you open a random file unrelated to the workspace root, it will not be able to find the root file and won't be able to resolve imports

[Mike Shulman]

Wouldn't it make more sense for the server to always be run from the directory where the file is?

[Mike Shulman]

And if I just open a file, without having opened any folder, what could the workspace root possibly be other than the folder where the file is?

[Mario Carneiro]

my understanding is that this is considered a niche use case. I believe lean 4 is even less willing to play along with non-project loose files

[Mario Carneiro]

honestly I can't think of very many programming languages that do

[Mike Shulman]

But my file is in a project; there is a leanpkg.path file in its directory. How am I supposed to guess that I have to tell VS Code to "open the project" rather than simply opening the file I want to work on?

[Mike Shulman]

I haven't used VS Code before, but I have programmed in many programming languages using Emacs, and in none of them did I ever have to do anything to edit a file, even one belonging to a "project", other than simply open that file.

[Julian Berman]

The reasoning I think at this point is just that no one has tweaked the root dir discovery in the VSCode Lean plugin to work the way you suggest -- in neovim it indeed works the way you mentioned (not sure about lean-mode). I think a PR to fix this for VSCode was welcome last time it was discussed, but I couldn't figure out the right VSCode APIs when I looked and gave up

[Patrick Massot]

Really that behavior of VSCode is a shame. I thought we added a warning message a long time ago. Did I dream that up?

[Kevin Buzzard]

There are warning messages -- e.g. on the community website, in the URL which appears to the user when an import fails.

[Patrick Massot]

I didn't dream the existence of https://github.com/leanprover/vscode-lean/blob/8ad0609f560f279512ff792589f06d18aa92fb3f/src/leanpkg.ts#L97-L100

[Patrick Massot]

Is it no longer working?

[Patrick Massot]

Maybe this is a bad side effect of having both the Lean3 and Lean4 VSCode extensions installed. Mike, do you have both extensions installed?

[Kevin Buzzard]

wooah now i am super-confused: if I use VS Code to open a random file in mathlib or lean-liquid then imports work?! The only difference is that the blue line at the bottom is now purple.

[Eric Rodriguez]

that's purple line is just vscode's default behaviour when a folder isn't open, afaik

[Kevin Buzzard]

"that" := "bottom line is purple" or "imports now work"?

[Eric Rodriguez]

bottom line is purple

[Mike Shulman]

I have only the Lean 3 extension installed.

[Mike Shulman]

The suggestion at https://leanprover-community.github.io/file-not-found.html is indeed what finally clued me into what was going on. You can certainly argue that I should have noticed it sooner. But I do think this is so counterintuitive that if it's really unfixable, the warning messages should be big and red on the front page about how to set up VS Code.

[Mike Shulman]

Patrick Massot said:

I didn't dream the existence of https://github.com/leanprover/vscode-lean/blob/8ad0609f560f279512ff792589f06d18aa92fb3f/src/leanpkg.ts#L97-L100

If I'm reading that code correctly, it just walks up through the parent directories of the workspace root looking for a leanpkg.path, and if it finds one, prompts the user to open that parent directory instead. I don't know what the workspace root is if I "open a file" directly, but if it's set to something arbitrary like / or $HOME, it's not going to find the correct directory that way.

[Eric Wieser]

Probably it should walk the parents of the open file instead?

[Eric Wieser]

I think the current behavior is because we have one global lean server per vscode window, and so therefore we need the workspace to agree on a single lean version, by putting leanpkg.toml in the root

[Eric Wieser]

A related task would be to make the refactor described at https://github.com/microsoft/vscode/wiki/Adopting-Multi-Root-Workspace-APIs

[Mike Shulman]

Thanks Eric, that makes a lot of sense for why the behavior is the way it is. In an ideal world, I would have expected that each bare file would have its own lean server, run from the location of that file. But maybe that's not practical.

Would it be possible to entirely forbid opening bare lean files in VS Code at all?

[Adam Topaz]

I don't think it's possible to forbid VScode from opening a single file.

[Mike Shulman]

But could the Lean extension refuse to run on a single file?

[Adam Topaz]

Yeah that's probably possible, but I don't know enough about the internals.

Anyway, one thing I do know for sure is that in emacs you can open a lean file and the package will figure out the root of the project dir.

[Mike Shulman]

Yeah -- obviously, since Emacs doesn't even have a notion of "open a folder".

[Adam Topaz]

right.

[Mike Shulman]

It's not hard to look at the location of a file and walk up the directory tree until you find a leanpkg.path.

[Junyan Xu]

In an ideal world, I would have expected that each bare file would have its own lean server, run from the location of that file. But maybe that's not practical.

Each new window does get its own Lean server. Editing a foundational file can be very slow when a leaf file (that depends on it) is open within the same window, due to the server compiling everything in between, so I usually just "duplicate workspace" which will open a new window.

[Mike Shulman]

That's a great example of why I don't like the "continuous compilation" design. It's cute when it's speedy, but when things get slow it is really annoying.

[Junyan Xu]

I heard that Lean 4 doesn't do that.

[Mike Shulman]

Doesn't do what?

[Floris van Doorn]

Lean 4 doesn't automatically propagate changes you made to other files to your current file. You have to manually refresh file dependencies in order to do this.
Lean 4 still does continuous compilation.
I agree that continuous compilation is annoying when it is slow, and I would have liked the Coq-style "step through proof" in certain long proofs. Lean 4 does support caching of intermediate goal states, so the continuous compilation should recompile a lot fewer steps each time.

[Junyan Xu]

This is where I heard that Lean 4 behaves differently, but I probably don't actually understand how it really behaves. With Lean 3 you can already select among six options (checking nothing / visible lines / visible lines and above / visible files / open files / project files) in VSCode, but none seems to help with the lagging issue when editing foundational file with a leaf file open. I assume if I select "checking nothing" then nothing will be compiled, but the dependencies are still being resolved after each keystroke? That seems to be the key factor in the lagging problem. Does Lean 4 behave differently in this aspect?

Lean 4 doesn't automatically propagate changes you made to other files to your current file. You have to manually refresh file dependencies in order to do this.

Does that mean Lean 4 will still use the list of open files to determine what to compile, but won't update dependency after each keystroke? Once you make an edit to the foundational file it will just compile up to / including all open files, and when you switch to the leaf file and refresh dependencies then you can immediately used what's compiled in the background?

[Mike Shulman]

Junyan Xu said:

With Lean 3 you can already select among six options (checking nothing / visible lines / visible lines and above / visible files / open files / project files) in VSCode

That's useful to know. Where are options like this documented?

[Junyan Xu]

Where are options like this documented?

I wonder too! I found this and this by Google search

[Junyan Xu]

It's also a useful trick that when working on a proof you can use sorry to prevent Lean from checking the rest of the proof (if there are multiple goals you need repeat {sorry}, and you can also sorry out blocks of codes enclosed by {} using sorry { ... }, when you don't want Lean to recheck a portion of proof you already completed.

[Bryan Gin-ge Chen]

The options are also (briefly) documented here: https://github.com/leanprover/vscode-lean#server-settings