Home of vscode-lean4

Stream: lean4

[Marc Huisinga]

I'm not particularly happy with the current home of vscode-lean4 at mhuisi/vscode-lean4. Ideally, I'd like the following to be true:

1. vscode-lean4 should be situated at leanprover-community.
2. Given that much of vscode-lean4 will include porting features from vscode-lean, the full history with all the original authors should be preserved.
3. Future improvements to vscode-lean should be ported to vscode-lean4 (e.g. the recent improvements to input.ts), also while preserving the original authors.
4. The extension should be published under leanprover, not under my mhuisi account.

I'd prefer to get this over with as soon as possible, so that mhuisi/vscode-lean4 does not widely establish itself as the URL for vscode-lean4 in documentation and elsewhere.

One difficulty is that I'm not sure how to satisfy (2) and (3).
At the moment, vscode-lean4 is intentionally minimal, both in terms of structure and configuration. Ideally, I'd like to keep it this way for the time being, and not litter the project with files that are being used in vscode-lean, but have not been ported yet as the corresponding server behaviour has not been implemented. Additionally, the extension was initially based on Microsoft's lsp-sample, not vscode-lean, and hence also includes its LICENSE.

What do you think would be the best way to go about this?

[Marc Huisinga]

(@Gabriel Ebner @Edward Ayers @Bryan Gin-ge Chen)

[Mario Carneiro]

Regarding (1), that can be handled by transferring ownership of the repo. Github will helpfully make mhuisi/vscode-lean4 a redirect for leanprover-community/vscode-lean4 in perpetuity (we did the same thing when moving leanprover/mathlib to the leanprover-community account).

[Mario Carneiro]

I've been thinking about whether it is possible to have vscode-lean and vscode-lean4 actually be the same extension, with some heuristics to figure out whether we are in lean 4 mode. That will make the user experience a lot smoother

[Marc Huisinga]

Mario Carneiro said:

I've been thinking about whether it is possible to have vscode-lean and vscode-lean4 actually be the same extension, with some heuristics to figure out whether we are in lean 4 mode. That will make the user experience a lot smoother

We could read leanpkg.toml and use languages.setTextDocumentLanguage or languages.setLanguageConfiguration. Note that as of now, vscode-lean4 does not really require users to open the project folder, although that may change as e.g. go to definition is implemented.

[Johan Commelin]

(2) can be solved by having a git repo with multiple roots in the git DAG, right?

[Eric Wieser]

Yes, but that only helps if you want to bring in all the lean3 files with it

[Eric Wieser]

Otherwise if you create that dag, delete all the files, then re-add them as you need them, git blame will just show when they were added

[Julian Berman]

Without being a specific solution, git-filter-repo is a (really the) thing that can help you filter some specific subset of files and preserve history: https://github.com/newren/git-filter-repo, but it can also get annoying if you at a later point want to add some additional file you didn't add at the beginning

[Julian Berman]

If you go the git-blame route (which I suspect is less annoying), git blame has a thing that lets you tell it revisions to ignore

[Julian Berman]

https://www.git-scm.com/docs/git-blame#Documentation/git-blame.txt---ignore-revs-fileltfilegt -- that -- so you could maintain some file with the revisions that cleared out the files

[Marc Huisinga]

I like the idea of integrating vscode-lean4 into vscode-lean and might take a stab at it when I find the time to. Some initial thoughts about what that would look like:

1. vscode-lean/extension.ts becomes extension_lean3.ts, vscode-lean4/extension.ts becomes extension_lean4.ts.
2. A new extension.ts file reads leanpkg.toml and activates either extension_lean3.ts or extension_lean4.ts depending on the Lean version in the TOML. I don't think leanpkg.ts is useful here, since it has a dependency to server.ts. There might end up being some duplicate code here that can be factored out later.
3. lean.* config options and commands remain as they are. The Lean 4 portion of the extension will reuse lean.* options/commands where possible and will declare its own Lean 4-exclusive options/commands as lean4.*.
4. Lean 3 will remain associated with the lean language id, whereas Lean 4 will be associated with the lean4 language id. Similarly, there will be language configurations and syntax files for each version. *.lean remains associated with the language id lean by default. If launched, extension_lean4.ts will set the language id of every newly opened file to be lean4.
5. Files that don't reference server.ts can probably be used immediately as-is, whereas files that depend on server.tswill need to be ported for the Lean 4 portion of the extension. To support both language versions, this might result in multiple ported files *_lean4.ts.

One might also consider running both language servers, e.g. in (4) if we decided to only set the language id to lean4 for files from within the project and Lean 3 files from outside the project are opened, or if users decide to set the language of a file to lean manually. I'm not sure how well that would work; it would probably require more changes to the Lean 3 part of the extension so that there's no accidental overlap between features and hence I'm in favor of disregarding this for now.

[Marc Huisinga]

(Whether Lean 4-exclusive options/commands need to be lean4.* is also debatable, I think :))

[Bryan Gin-ge Chen]

Having a single extension for both Lean 3 and Lean 4 sounds like it would make things easiest for users at the cost of some integration pain for developers, which I personally think would be worth the effort. Points 1-5 above look like a reasonable plan to me, but I'd like to hear what @Gabriel Ebner thinks.

P.S. I'm happy to help out to the extent I can, but I'm not familiar enough with the Lean 4 server yet to build much on my own. (Would be very interested in learning more about it though!) Feel free to ping me for questions or review.

[Gabriel Ebner]

@Marc Huisinga I think your approach looks good. The main benefit I expect from integrating both extensions is that it makes it easier to use both Lean 3 and Lean 4. I believe the only code that would be initially shared by both extensions would be the input mode. Eventually, the infoview might be shared as well.

[Gabriel Ebner]

One potential downside is that we'll need to keep the Lean 3 part of the extension virtually forever.

[Gabriel Ebner]

Maybe we should keep them separate after all, but still support installing them side-by-side (and running them at the same time in a workspace).

[Marc Huisinga]

I don't have a strong opinion on this, except that integrating the two makes it easier for me to preserve the git history of files like input.ts and use improvements to it in the future :)

[Gabriel Ebner]

I'm perfectly happy to backport / forwardport PRs between the extensions myself if necessary, that shouldn't influence the decision.

[Gabriel Ebner]

My suggestion for the "separate" approach would be to make one commit on top of the vscode-lean extension, which ontains the current changes of vscode-lean4, and then move out all the files that are not ported yet to a separate directory where they are not compiled. This should result in straightforward merge PRs.

[Gabriel Ebner]

I think it's unrealistic to expect much code sharing between the two extensions, both now and in the long run.

[Marc Huisinga]

(and running them at the same time in a workspace).

This is difficult. My proposal suggests that all *.lean files are identified according to the version specified in the leanpkg.toml. Users can set the version of a single file manually, but does that really work well with vscode-lean? I vaguely remember plenty of things only working well when you launch vscode-lean at the workspace-level.

[Marc Huisinga]

If we went for the "separate extensions" approach, I'd imagine that it would work somewhat similar to my earlier proposal: Both extensions read the leanpkg.toml and activate depending on the version.

[Gabriel Ebner]

My main concern is that keeping the two extensions together is a lot of technical debt: Lean 3 server mode is essentially frozen (for compatibility reasons). In a year or two from now, virtually nobody will use Lean 3 anymore but we'll still have lots of dead code in the repo. Which we can't remove because one or two people will still want to look at old mathlib versions.

[Gabriel Ebner]

extension_lean4.ts will set the language id of every newly opened file to be lean4.

Is there a reason this won't work for two separate extensions?

[Marc Huisinga]

Gabriel Ebner said:

extension_lean4.ts will set the language id of every newly opened file to be lean4.

Is there a reason this won't work for two separate extensions?

It does, as suggested right above :)

[Gabriel Ebner]

Users can set the version of a single file manually, but does that really work well with vscode-lean?

If I set the language type to C++, then the Lean 3 extensions seems to shut up. It might still start the Lean server, but we can probably fix this.

[Gabriel Ebner]

If we went for the "separate extensions" approach, I'd imagine that it would work somewhat similar to my earlier proposal: Both extensions read the leanpkg.toml and activate depending on the version.

This is probably the most reasonable approach.

[Marc Huisinga]

Right, that's not the issue. I'm wondering whether it's actually possible to reasonably run both language servers at once for the same workspace, and have vscode-lean do reasonable things when the project is a lean4 project, but the user sets some file to be lean3. The alternative is the conditional approach from my proposal, where only one server is active at a time.

[Gabriel Ebner]

Ah, so there are two questions here:

1. Should there be two extensions?
2. Should they be able run in a single project at the same time?

[Gabriel Ebner]

I'm not sure 2) matters very much. If we want to do hybrid projects, we can always put them in subdirectories.

[Sebastian Ullrich]

What about mathlib porting though...? :)

[Gabriel Ebner]

The hybrid approach as suggested by Leo would just have two directories: mathlib/lean3 and mathlib/lean4. Plus a script that compiles the lean3 directory into lean4/MathlibOld.olean or something.

[Gabriel Ebner]

Putting both in the same directory doesn't work seamlessly either: elan picks the lean version based on leanpkg.toml. And there's only one version field there.

[Mario Carneiro]

Gabriel Ebner said:

My main concern is that keeping the two extensions together is a lot of technical debt: Lean 3 server mode is essentially frozen (for compatibility reasons). In a year or two from now, virtually nobody will use Lean 3 anymore but we'll still have lots of dead code in the repo. Which we can't remove because one or two people will still want to look at old mathlib versions.

It's not dead code until the users are not using it anymore. All indications are that this won't happen for a long while. If/when we get to a point where we can drop support for it, it can be moved to a separate extension (assuming you want to keep some lean 3 extension on the marketplace in perpetuity) based on a frozen version of the current one

[Mario Carneiro]

Also, I think it is possible to share more code if the lean 3 part of the code is just a shim to make the communication roughly compatible with the LSP interface

[Gabriel Ebner]

If we want to separate the extensions anyhow, then why merge them in the first place? From my point of view, the only real advantage is that the input mode can be shared. Everything else will and should probably be independent anyhow.

[Mario Carneiro]

Having them as separate installed extensions means that they compete for "ownership" of the files. VSCode wants to associate an extension to the .lean file extension

[Marc Huisinga]

Mario Carneiro said:

Having them as separate installed extensions means that they compete for "ownership" of the files. VSCode wants to associate an extension to the .lean file extension

This is not an issue, we can activate either extension conditionally depending on leanpkg.toml as in the earlier proposal and dynamically associate *.lean files with Lean 4.

[Mario Carneiro]

Having them both in one extension means that the lean 3/4 determination is up to the extension, which I think will be necessary

[Gabriel Ebner]

Mario Carneiro said:

Having them both in one extension means that the lean 3/4 determination is up to the extension, which I think will be necessary

I agree that this is necessary. But it is also completely independent of whether there's one or two extensions.

[Mario Carneiro]

So the lean 3 extension thinks that all lean files are lean 3 and the lean 4 extension is conditionally activated? How does that work with things like syntax highlight?

[Marc Huisinga]

Mario Carneiro said:

So the lean 3 extension thinks that all lean files are lean 3 and the lean 4 extension is conditionally activated? How does that work with things like syntax highlight?

Syntax highlighting is bound to the language id, not the file extension. I've already done and tested this stuff in my local fork of vscode-lean, I only need to integrate the conditional leanpkg.toml stuff.

[Gabriel Ebner]

Mario Carneiro said:

Also, I think it is possible to share more code if the lean 3 part of the code is just a shim to make the communication roughly compatible with the LSP interface

There's enough differences that it's not easy to paper over them with a shim. For example: Lean 4 doesn't rebuild dependencies by itself. Lean 3 has a specific widget protocol, etc.
Either you make Lean 3 users angry by taking away Lean 3 features, or you make Lean 4 users angry by not supporting better protocols.

[Mario Carneiro]

Lean 4 doesn't rebuild dependencies by itself

So you have a "rebuild dependencies" command that is a no op for one of them

Lean 3 has a specific widget protocol

I hope that lean 4 gets one too (in the meantime it can be a no op)

[Marc Huisinga]

Gabriel Ebner said:

If we want to separate the extensions anyhow, then why merge them in the first place? From my point of view, the only real advantage is that the input mode can be shared. Everything else will and should probably be independent anyhow.

One advantage (which I'm not sure matters much) is that we could eventually seamlessly turn vscode-lean into the Lean 4 extension and factor out the Lean 3 part into a vscode-lean3 extension, whereas if we use two separate extensions, the Lean 4 extension would likely always remain vscode-lean4, which could result in confusion.

[Gabriel Ebner]

We can rename the "lean" extension to "lean 3" today. That shouldn't be the issue here.

[Marc Huisinga]

Ok :)

[Sebastian Ullrich]

As long as it's leanprover/lean4, vscode-lean4 seems appropriate

[Gabriel Ebner]

@Mario Carneiro The new widget protocol will probably look different from the current one. Obvious cleanups aside, e.g. there's currently no way to keep a widget when a file is recompiled.
But we're getting away from the main issue here. Writing (and maintaining) a compatibility shim for Lean 3 is a dead end and having to support it indefinitely is technical debt.

[Mario Carneiro]

perhaps eventually, but good lean 3/4 integration is very important during the transition period, and I think the transition period will be quite long (>1 year) so it seems like a worthwhile investment

[Gabriel Ebner]

I am very happy that we don't have to support Lean 2 in the vscode extension.

[Marc Huisinga]

(i surrender at trying to understand zulip polls)

[Gabriel Ebner]

From what Marc has found out, there doesn't seem to be any technical advantage to integrating both extensions. We can and need to use exactly the same mechanism (manually setting language ids and parsing leanpkg.toml) in both cases.

[Sebastian Ullrich]

Fwiw, for the handful of Emacs users I'll just assume they're happy with using a separate editor instance per Lean version, which emacs --eval makes easy enough to set up (which is exactly what nix run .#emacs-dev is doing).

[Mario Carneiro]

vscode doesn't like it when you open the same folder twice, so as long as the vscode-lean4 extension takes over use of the lean extension as it does currently, it can't be used for hybrid projects

[Gabriel Ebner]

@Mario Carneiro What are your thoughts on leanpkg.toml for hybrid projects. Both 3 and 4 in the same toml? Two subdirectories for 3/4, and one toml per subdirectory?

[Mario Carneiro]

will it work if you manually set the language ID?

[Mario Carneiro]

My original hope was for the files themselves to indicate the language, e.g. via #lang lean3

[Mario Carneiro]

It could be one toml or two, I don't think it makes a big difference. One toml per subdirectory would be a big change from the current setup though

[Mario Carneiro]

since right now you don't have to declare the list of files in a project

[Gabriel Ebner]

I mean mathlib/lean3/leanpkg.toml and mathlib/lean4/leanpkg.toml.

[Gabriel Ebner]

The reason I'm asking is this:

$ grep lean_version leanpkg.toml
lean_version = "leanprover-community/lean:3.24.0"

[Mario Carneiro]

Oh, that might work, although if the lean3 files call the lean4 files and vice versa it's an interesting task to figure out how to get everything compiling

[Gabriel Ebner]

I'm not sure if vice versa is necessary. We can just start porting at the leaves.

[Mario Carneiro]

wasn't there talk of using oleans to communicate both ways?

[Mario Carneiro]

(in the lean 4 logic)

[Mario Carneiro]

I think it's easier to start porting from the root, since there will be competition for basic things like Nat vs nat otherwise

[Gabriel Ebner]

Clearly, the olean converter needs to adapt the naming convention as well.

[Mario Carneiro]

that's not all though, it needs to be logic-equivalent and that's surely not going to be the case

[Mario Carneiro]

it will probably work okay for a lot of things but your average leaf file will almost certainly depend on at least one of the exceptions

[Gabriel Ebner]

I'm not sure I understand completely what "logic-equivalent" is. You obviously need to map and to And, and iff to Iff, and quot to Quot, and classical.choice to Classical.choice.

[Mario Carneiro]

I haven't looked at all the details of lean 4 definitions, but I would assume that they vary in at least a few places. For example Add has more arguments than has_add, there is more stuff with boolean equality and less with decidability, and other things of that nature. It's not a literal 1-1 replacement even if you fix the naming scheme

[Kevin Lacker]

are all the inheritance hierarchies going to be exactly the same between lean 3 and lean 4

[Mario Carneiro]

so in some leaf file about topological rings you will have has_add from lean 3 stuff and Add from lean 4 stuff and no theorems that relate them

[Gabriel Ebner]

Add is actually the same. HAdd is new and different.

[Gabriel Ebner]

There are some really gratuitious argument order changes though:

-- Lean 3:
def ite (c : Prop) [h : decidable c] {α : Sort u} (t e : α) : α :=
-- Lean 4:
def ite {α : Sort u} (c : Prop) [h : Decidable c] (t e : α) : α :=

[Kyle Miller]

Gabriel Ebner said:

Add is actually the same. HAdd is new and different.

This might be something to watch out for:

theorem comm1 (x y : α) [HAdd α α β] : HAdd.hAdd x y = HAdd.hAdd y x := sorry
theorem comm2 (x y : α) [Add α] : Add.add x y = Add.add y x := sorry

example (x y z : α) [Add α] : x + y + z = y + x + z := by
    rw comm1 x -- OK

example (x y z : α) [Add α] : x + y + z = y + x + z := by
    rw comm2 x -- Fails

[Gabriel Ebner]

I'm not sure if this will be a huge problem in practice. Typically both Add and HAdd should come from CommMonoid or something, and then they're defeq.

[Sebastian Ullrich]

Except when doing keyed matching e.g. in simp (edit: or rw as above) :silence: . Ideally the operators should not be mixed.

[Kyle Miller]

I just mean if there's an interface to import Lean 3 oleans, then if somehow there's a mapping has_add.add -> Add.Add, this test suggests you won't be able to use those lemmas with rw without some more work.

[Gabriel Ebner]

Ah, so if I understand this correctly, Add.add is a forbidden constant that shouldn't be used. Kind of like comm_monoid.mul now.

[Sebastian Ullrich]

Heterogeneous operators are very expressive, but that, as usual, does come with a few surprises in practice. So really there should be one more experiment on whether the current encoding of heterogeneous operators with default instances works for mathlib or not. But once there has been a decision, people should stick with it to avoid rewriting issues, yes. Or they will need to call a tactic normalizing homogeneous to heterogeneous operators first.

[Kevin Buzzard]

By the way Sebastian -- we've been using homogeneous * for years now in Lean 3, but occasionally we want an object to act on another object, and for this we often use mathlib's

class has_scalar (α : Type u) (γ : Type v) := (smul : α → γ → γ)

which is tied to different notation ( • a.k.a. \bub).

[Mohamed Al-Fahim]

Should new feature PRs be made to https://github.com/mhuisi/vscode-lean4 or to https://github.com/leanprover/vscode-lean? I have implemented unicode autocomplete for https://github.com/mhuisi/vscode-lean4, and am not sure whether to implement it for https://github.com/leanprover/vscode-lean too.

Lean-Unicode-Completion.gif

[Gabriel Ebner]

Input-related PRs should go to vscode-lean for the forseeable future.

[Eric Wieser]

Isn't there already an open PR against vscode-lean for unicode autocomplete?

[Marc Huisinga]

[With the leanprover/lean4 master, all LSP clients now support displaying the type and documentation on hover]

[Super Veridical]

Would I be correct in saying that neither "lean4-mode" for emacs nor vscode-lean4 currently support proof-state/goal display?

[Julian Berman]

I guess my limited C++ skills are failing me since I can't seem to compile master on macOS, cmake is complaining about fatal error: 'stdlib.h' file not found once it gets to compiling stage1 which IIRC is something usually about it using the wrong sysroot on macOS or somethign right? I'm using normal clang++ as it looks like the lean4 docs recommend.

[Marc Huisinga]

Julian Berman said:

I guess my limited C++ skills are failing me since I can't seem to compile master on macOS, cmake is complaining about fatal error: 'stdlib.h' file not found once it gets to compiling stage1 which IIRC is something usually about it using the wrong sysroot on macOS or somethign right? I'm using normal clang++ as it looks like the lean4 docs recommend.

Alternatively you can also download the artifact directly: https://github.com/leanprover/lean4/runs/1712478947 ("Artifacts" in the top right corner)

[Julian Berman]

Ah cool thanks!

[Julian Berman]

@Marc Huisinga prettyyyy :) it works, thanks!

[Sebastian Ullrich]

No need for that, everything should be contained in the latest nightly: https://github.com/leanprover/lean4-nightly/releases/tag/nightly-2021-01-16

[Marc Huisinga]

PR for compat with vscode-lean4: https://github.com/leanprover/vscode-lean/pull/253

[Marc Huisinga]

To conclude this thread:

• vscode-lean4 has moved to leanprover-community/vscode-lean4
• The extension can now be found under the ID leanprover.lean4 on the marketplace
• mhuisi.lean4, the old version of vscode-lean4 that was published on my user account, has been unpublished
• The version of vscode-lean4 that is published at leanprover.lean4 can be run at the same time as vscode-lean
• @Wojciech Nawrocki added server support for go to definition :)

[Sebastien Gouezel]

I just installed Lean 4 to play a little bit with it. No problem to install the VScode extension, thanks a lot! Just a small issue with the go to definition feature: it seems it doesn't try to open the right file, so it doesn't find it. Possibly related to the fact that I'm on windows. The output is like

Impossible d'ouvrir 'Prelude.lean' : Impossible de lire le fichier '\\c:\Users\Sebastien\.elan\toolchains\leanprover-lean4-nightly\bin\Users\Sebastien\.elan\toolchains\leanprover-lean4-nightly\lib\lean\src\Init\Prelude.lean' (Unknown (FileSystemError): Error: UNKNOWN: unknown error, stat '\\c:\Users\Sebastien\.elan\toolchains\leanprover-lean4-nightly\bin\Users\Sebastien\.elan\toolchains\leanprover-lean4-nightly\lib\lean\src\Init\Prelude.lean').

The right file to open would be \\c:\Users\Sebastien\.elan\toolchains\leanprover-lean4-nightly\lib\lean\src\Init\Prelude.lean, and the Lean location is \\c:\Users\Sebastien\.elan\toolchains\leanprover-lean4-nightly\bin. It seems it tries to concatenate the two to find the file name.

[Sebastian Ullrich]

Huh, interesting! @Wojciech Nawrocki Any idea? Since the error seems to be from VS Code, fileWithExt must have succeeded. Prefixing that backslash-separated path with file:// afterwards is probably incorrect, though I'm not sure how it could lead to this duplication.

[Wojciech Nawrocki]

Just getting set up on Windows and I get this:

$ which leanpkg
/c/Users/Wojtek/Desktop/\Users\Wojtek/.elan/bin/leanpkg

which looks suspiciously similar but it's just the shell.

[Wojciech Nawrocki]

Well, I played with Lean 4 on Windows and I'm amazed you got as far as go-to-def :rolling_on_the_floor_laughing: The actual bug appears to be that file://host/fname means "fname on remote host host", so VSCode interprets c: as a network share and then who knows what happens. For me, the editor crashes with an OOM/infinite loop. PR'd a fix that should appear in the nightly in a few days. My Windows setup is unfortunately incredibly painful to work with, so I will not be able to look at Windows any more until I resolve that.

[Sebastien Gouezel]

Just to confirm that with the last nightly the problem is solved on my computer. Thanks!