Zulip Chat Archive

Stream: lean4

Topic: Home of vscode-lean4


view this post on Zulip 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.

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

view this post on Zulip Marc Huisinga (Jan 09 2021 at 12:01):

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

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Marc Huisinga (Jan 09 2021 at 18:00):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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 :)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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 :)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Sebastian Ullrich (Jan 11 2021 at 16:27):

What about mathlib porting though...? :)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Marc Huisinga (Jan 11 2021 at 16:51):

Ok :)

view this post on Zulip Sebastian Ullrich (Jan 11 2021 at 16:55):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Marc Huisinga (Jan 11 2021 at 16:57):

(i surrender at trying to understand zulip polls)

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Jan 11 2021 at 17:02):

will it work if you manually set the language ID?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jan 11 2021 at 17:05):

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

view this post on Zulip Gabriel Ebner (Jan 11 2021 at 17:05):

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

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jan 11 2021 at 17:08):

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

view this post on Zulip Mario Carneiro (Jan 11 2021 at 17:08):

(in the lean 4 logic)

view this post on Zulip 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

view this post on Zulip Gabriel Ebner (Jan 11 2021 at 17:10):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Gabriel Ebner (Jan 11 2021 at 17:20):

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

view this post on Zulip 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 : α) : α :=

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip Gabriel Ebner (Jan 13 2021 at 08:47):

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

view this post on Zulip Eric Wieser (Jan 14 2021 at 12:05):

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

view this post on Zulip 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]

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Julian Berman (Jan 16 2021 at 15:44):

Ah cool thanks!

view this post on Zulip Julian Berman (Jan 16 2021 at 15:48):

@Marc Huisinga prettyyyy :) it works, thanks!

view this post on Zulip 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

view this post on Zulip Marc Huisinga (Jan 17 2021 at 22:26):

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

view this post on Zulip 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 :)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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