Stream: lean4

Topic: Home of vscode-lean4

Marc Huisinga (Jan 09 2021 at 11:58):

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.

Marc Huisinga (Jan 09 2021 at 12:01):

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

Mario Carneiro (Jan 09 2021 at 12:10):

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 (Jan 09 2021 at 12:12):

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 (Jan 09 2021 at 12:37):

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 (Jan 09 2021 at 13:56):

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

Eric Wieser (Jan 09 2021 at 15:07):

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

Eric Wieser (Jan 09 2021 at 15:08):

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 (Jan 09 2021 at 17:11):

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 (Jan 09 2021 at 17:12):

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 (Jan 09 2021 at 17:13):

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 (Jan 09 2021 at 17:44):

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 (Jan 09 2021 at 18:00):

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

Bryan Gin-ge Chen (Jan 09 2021 at 20:57):

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 (Jan 11 2021 at 16:02):

@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 (Jan 11 2021 at 16:02):

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

Gabriel Ebner (Jan 11 2021 at 16:04):

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 (Jan 11 2021 at 16:06):

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 (Jan 11 2021 at 16:07):

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

Gabriel Ebner (Jan 11 2021 at 16:10):

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 (Jan 11 2021 at 16:11):

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

Marc Huisinga (Jan 11 2021 at 16:14):

(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 (Jan 11 2021 at 16:17):

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 (Jan 11 2021 at 16:20):

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 (Jan 11 2021 at 16:21):

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 (Jan 11 2021 at 16:22):

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 (Jan 11 2021 at 16:23):

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 (Jan 11 2021 at 16:24):

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 (Jan 11 2021 at 16:24):

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 (Jan 11 2021 at 16:26):

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 (Jan 11 2021 at 16:26):

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

Sebastian Ullrich (Jan 11 2021 at 16:27):

What about mathlib porting though...? :)

Gabriel Ebner (Jan 11 2021 at 16:28):

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 (Jan 11 2021 at 16:29):

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 (Jan 11 2021 at 16:36):

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 (Jan 11 2021 at 16:38):

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 (Jan 11 2021 at 16:38):

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 (Jan 11 2021 at 16:40):

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 (Jan 11 2021 at 16:41):

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 (Jan 11 2021 at 16:41):

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 (Jan 11 2021 at 16:41):

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 (Jan 11 2021 at 16:43):

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 (Jan 11 2021 at 16:44):

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 (Jan 11 2021 at 16:44):

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 (Jan 11 2021 at 16:45):

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 (Jan 11 2021 at 16:46):

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 (Jan 11 2021 at 16:50):

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

Ok :)

Sebastian Ullrich (Jan 11 2021 at 16:55):

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

Gabriel Ebner (Jan 11 2021 at 16:55):

@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 (Jan 11 2021 at 16:56):

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 (Jan 11 2021 at 16:56):

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

Marc Huisinga (Jan 11 2021 at 16:57):

(i surrender at trying to understand zulip polls)

Gabriel Ebner (Jan 11 2021 at 16:57):

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 (Jan 11 2021 at 16:58):

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 (Jan 11 2021 at 17:00):

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 (Jan 11 2021 at 17:02):

@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 (Jan 11 2021 at 17:02):

will it work if you manually set the language ID?

Mario Carneiro (Jan 11 2021 at 17:03):

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

Mario Carneiro (Jan 11 2021 at 17:04):

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 (Jan 11 2021 at 17:05):

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

Gabriel Ebner (Jan 11 2021 at 17:05):

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

Gabriel Ebner (Jan 11 2021 at 17:06):

The reason I'm asking is this:

$grep lean_version leanpkg.toml lean_version = "leanprover-community/lean:3.24.0"  Mario Carneiro (Jan 11 2021 at 17:07): 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 (Jan 11 2021 at 17:07): I'm not sure if vice versa is necessary. We can just start porting at the leaves. Mario Carneiro (Jan 11 2021 at 17:08): wasn't there talk of using oleans to communicate both ways? Mario Carneiro (Jan 11 2021 at 17:08): (in the lean 4 logic) Mario Carneiro (Jan 11 2021 at 17:09): 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 (Jan 11 2021 at 17:10): Clearly, the olean converter needs to adapt the naming convention as well. Mario Carneiro (Jan 11 2021 at 17:10): that's not all though, it needs to be logic-equivalent and that's surely not going to be the case Mario Carneiro (Jan 11 2021 at 17:11): 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 (Jan 11 2021 at 17:14): 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 (Jan 11 2021 at 17:18): 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 (Jan 11 2021 at 17:18): are all the inheritance hierarchies going to be exactly the same between lean 3 and lean 4 Mario Carneiro (Jan 11 2021 at 17:20): 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 (Jan 11 2021 at 17:20): Add is actually the same. HAdd is new and different. Gabriel Ebner (Jan 11 2021 at 17:22): 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 (Jan 11 2021 at 17:26): 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 (Jan 11 2021 at 17:30): 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 (Jan 11 2021 at 17:33): Except when doing keyed matching e.g. in simp (edit: or rw as above) :silence: . Ideally the operators should not be mixed. Kyle Miller (Jan 11 2021 at 17:34): 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 (Jan 11 2021 at 17:49): 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 (Jan 12 2021 at 14:00): 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 (Jan 12 2021 at 15:08): 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 (Jan 13 2021 at 08:12): 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 (Jan 13 2021 at 08:47): Input-related PRs should go to vscode-lean for the forseeable future. Eric Wieser (Jan 14 2021 at 12:05): Isn't there already an open PR against vscode-lean for unicode autocomplete? Marc Huisinga (Jan 16 2021 at 13:02): [With the leanprover/lean4 master, all LSP clients now support displaying the type and documentation on hover] Super Veridical (Jan 16 2021 at 14:00): Would I be correct in saying that neither "lean4-mode" for emacs nor vscode-lean4 currently support proof-state/goal display? Julian Berman (Jan 16 2021 at 15:41): 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 (Jan 16 2021 at 15:43): 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 (Jan 16 2021 at 15:44): Ah cool thanks! Julian Berman (Jan 16 2021 at 15:48): @Marc Huisinga prettyyyy :) it works, thanks! Sebastian Ullrich (Jan 16 2021 at 15:48): 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 (Jan 17 2021 at 22:26): PR for compat with vscode-lean4: https://github.com/leanprover/vscode-lean/pull/253 Marc Huisinga (Jan 26 2021 at 10:16): 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 (Jan 26 2021 at 20:50): 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 (Jan 26 2021 at 22:00): 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 (Jan 26 2021 at 23:05): 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 (Jan 27 2021 at 06:18):

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 (Jan 29 2021 at 06:34):

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

Last updated: May 07 2021 at 12:15 UTC