Re-enables auto-downloading of Lean via elan, and add Select Interpreter
#35
Conversation
…nel so we can better debug the issue of \ sometimes not wroking.
…is workspace specific. fix: auto open of infoview should only happen once per vscode session. fix: auto open of infoview should not happen on markdown files.
lovettchris
changed the title
There was a problem hiding this comment.
This PR contains afaict at least three different changes, some of which I'm very positive about and others which I'm not so positive about. These should be three or four separate PRs:
- Showing errors from the abbreviation rewriter in an output panel.
- Preventing the infoview from opening automatically for markdown files.
- The select interpreter dropdown.
- Ignoring some errors in the infoview<->extension api.
(1) looks good to me. The abbreviations code is notoriously flaky. It would be great if users would see the errors as well so that they can report bugs.
(2) also looks good to me (but the fix is buried in other changes).
(3) I'm not sure if this is such a good idea. With this change, we'd have three ways to select the interpreter:
a) The version field in the leanpkg.toml field (used by elan)
b) The lean.executablePath setting
c) The executable selected in the interpreter dropdown.
It doesn't help that each of these three options uses a different terminology (version vs executable vs interpreter). Option a) is the preferred one, and we should forcefully nudge users in that direction. If we can't find lean, we should tell the user to install elan (or offer to automatically install it, like we did in the Lean 3 extension).
(4) This change seems very contrary to the infoview design. If there are problems with the infoview when the server crashes (or isn't started yet), then that should probably be fixed on the infoview side.
|
@gebner, Hi Gabriel, is there any way I can chat with you overall about the extension and coordinate a bit with you now that you are back from vacation? Does Tulip do voice chat? Or I could send a Teams invite or something. There's a good reason I'm pushing for a "select interpreter" dropdown. I'm modeling this on the Python extension, we can name the command whatever you want, but what I'm finding is that one global setting isn't right. When I have my local Windows box, WSL and a remote SSH setup the path needs to be different for all three of these environments. So to me it makes more sense for it to be sort of "vscode workspace" specific, not in a project file you check into a repo, and not global to vscode... so that's where I landed using a command and then storing that in vscode "workspace settings". Having a global default is still fine, and the default non-full-path value of "lean" is a great default. The "version" you mentioned in the package file could also inform the select interpreter command where it could check the selected path does match the package version requested... |
Sorry about that, I can break it up into separate PR's if you like. |
I think it's best to arrange a time on zulip. I believe there's quite a bit of timezone difference between us. You can start a video meeting on zulip (via jitsi) but teams is fine as well.
Yes please. |
|
I agree with @gebner 's review that it would be best to split this into a few PRs. The select interpreter functionality does seem useful for working with multiple environments, but it should be clear that the point is to tell VSCode where to find elan, rather than which version of Lean to use (I agree the |
I have split out 2 new PR's, I'll rebase this one once those are merged. |
lovettchris
changed the title
Select Interpreter
|
@gebner , I'm not sure how to fix this build error... |
… has set a different default.
This was weird, I couldn't reproduce the bug at first. I could only reproduce it after cleaning the vscode-lean4 directory. I'm not 100% certain what went wrong here. My best guess is that some dependency used to include |
|
@gebner oh, cool "all checks have passed" are you good with merging this PR now? Note, I found a fix for a random problem I was seeing when restarting the lean server, |
… vscode-languageclient version 8.0.0 as per recommendation from microsoft/vscode-languageserver-node#825 this also means we've moved to vscode-languageserver-protocol 3.17. Everything seems to work, but probably needs more testing...
…e-lean4 into clovett/logging_errors
I would be a bit more emphatic here: setting the default toolchain to a specific version is a very bad idea. The default toolchain should be a distro (i.e., Also, more generally, aren't we trying to migrate away from |
Yes, but I want to add Lake support in a separate PR, since I'm being told this PR is already too big. Note the PR started before Lake was even checked in... As for the "default" toolchain question, I see I can set a default toolchain using (the last one is a symlink to my local build that I created manually). |
My point isn't that this should add
That's weird. Still, if this extension is installing TL;DR: my point is just drop the |
I'm not really adding But the extension is definitely not promoting leanpkg in any way, it does not offer to run it, or build it or anything, it's just trying to figure out the version that but re-reading your point here:
I think I understand, it is all about setting the |
The problem here is that this shouldn't be fixed. This is the intended behavior of elan. It first installs a general distro to use wherever and then it installs a specific version to use in the current workspace. If VSCode was installing elan just for the current workspace (e.g., in a Gitpod instance), installing a single version would make sense. But it isn't, it is installing elan generally. Thus, it should also install a global default toolchain. Also, as one of the main reasons to package |
|
Mathlib is a good example, it is using Note: this cost of double installation will become even more noticeable when we enable github codespaces, since every new codespace will do a new install. I don't want every one of those new codespaces to install 2 versions of lean if it is not really necessary. |
You are making this sound like installing a toolchain is a particularly time intensive process. It generally takes ~5-10s (at most). Most installers take a good minute or two to walk through, so asking the user to spends (at worst) 20s installing
The default toolchain isn't for when you are inside a project. It is specifically for use when one is working outside of a project without a specific lean version. For example, I have folder named
Isn't there some way we can detect if we are in codespace and only in that particular case install elan without a default toolchain? Alternatively, the prompt to automatically install elan/Lean could have 3 options: More generally, I personally don't see the issue with installing 2 toolchains. First, as a user, when prompted to isntall elan/Lean is automatically by VSCode, I would expect it to be installed in a way that is globally functional (unless otherwise noted), not in a way that is only functional for particular projects. Second, I don't see 20s as a major cost for an install. Regardless, if you don't want elan to install a default toolchain, it should be installed with |
…-toolchain to something specific.
|
You must have a much faster network than my piddly little comcast home network where install is taking longer. I did have |
😆! I was quoting times from the CI/CDs across various Lean projects. Admittedly, that may be a little unfair as it is a GitHub service talking to GitHub service, but I imagine the various GitHub servers are not necessarily all geographically close, so it may still be a reasonable metric. And it is also fast on my pretty old (though quite high-end) Windows machine.
It's better, I still personally think it should install things in the same manner one would do manually (i.e., install a distro and then install the specific toolchain for a given project), but I am not the last word on this. |
|
How about some text like "This project uses Lean version {}. We recommend also installing the Lean 4 nightly release (which can be updated via |
|
I strongly believe that we shouldn't set a default toolchain for elan. This has caused lots of troubles in the past. No matter how you set it up, users will end up with an outdated toolchain and wonder why things are subtly broken. If you set I'd rather tell people to use
@tydeu Please realize that not everybody is on a high-speed, unmetered connection all the time and has money to spend on a lot of disk space. A lot of people are working from trains, mobile connections, airport wifi, etc. The Lean 4 releases are already huge (over 100 megabytes), and if we merge leanprover/lean4#733 then they'll almost double in size. |
Good points. I am happy to settle for this.
Fair enough. However, even if one has a really bad internet connection and it takes many minutes, this is a one-time install. Thus, as an end user myself, I would think it perfectly reasonable to have wait some time for things to get setup. Also, how is 100/200MBs huge? Games can easily be many gigs to install, and big software libraries (like LLVM) and most IDEs can be many hundreds of MBs (e.g., 500MB-1GB) mark. For example, VSCode is a rather lightweight IDE, but even its installer is 50MBs by itself (i.e., not counting the things it downloads or the extensions it installs on startup). Thus, were we going down that route, I think Also, until Lean 4 has a widely use stable release, an end user will likely have install a new toolchain for each project they open (as they are likely to all be on slightly different nightlies that will frequently change), so they will have to get use to multiple toolchain downloads regardless. |
Please read again what I've written. What's a small download for you can be a lengthy download for somebody else. Not everybody has access to a high-speed internet connection. And as you said, a single Lean release is more than twice as large as a certain editor that literally bundles a whole web browser. The initial setup feature targets newbies who are not yet invested in the Lean ecosystem (otherwise they would have installed elan manually). I don't really want to make someone download a few hundred megabytes extra just to try out Lean if it's not strictly necessary.
It's not like I'm excited about that, my elan directory is already over 10 gigabytes large (and that's after removing some old nightlies...). Bundling clang for every nightly isn't going to make that better either. |
I feel like we may be talking a cross paths here. I already assented to the fact the such downloads could be lengthy. Also, Chromium is a surprisingly lightweight piece of software -- compressed it is only a little over 50MBs and uncompressed it is little over 200MBs. Note that VSCode installer manages to somehow still be less than this, so I suspect it strips some pieces, does some interesting compression tricks, and/or downloads additional data during install. I also gave a number of common heavyweight examples -- including LLVM, which, by itself, is still a bigger bundle than both Lean and clang/lld/etc.
I tended to think of the automatic Also, I still do not get the quibbling over a few hundred MBs. For example, Rust's toolchain downloads are 250-350MBs, the average IntelliJ IDEA IDE installer is 400-600 MBs and Visual Studio is GBs. I would think most end users would be familiar with installing a few hundred MBs packages to get things up and running, and I feel like I have a good bit of evidence to defend that point. |
|
Regardless, this is all tangential, right? I seems to me that the conclusion we have come to is for VSCode to install elan without a default toolchain and let then install the toolchain for the opened workspace itself. Users will then need to install a default toolchain of their own or use elan's |
Yes, I think Gabriel and I are in sync and the current bits in this PR will do the right thing during the bootstrap process, starting from scratch with no .elan installed, it will try not to install multiple toolchains and it will try not to set --default-toolchain. |
Co-authored-by: Gabriel Ebner <[email protected]>
feat: Re-enables auto-downloading of Lean via
elanfeat: Adds progressive output from
lean --versionwhich can take a while when it has to install the requested verison.feat: Add
Lean 4: Select Interpreterfor quick and easy overriding of the lean version, particularly useful while developinglean4locally and makes it possible again to get lean intellisense in a folder that has no leanpkg.toml file.fix: Change
LeanClientso it can "restart" the server without needing to recreate LeanClient, this ensures you still get Lean syntax coloring even iflean --servercannot be started and it makes the above scenarios work more smoothly.fix: Error [ERR_STREAM_WRITE_AFTER_END]: write after end by moving to vscode-languageclient version 8.0.0.
added 10/11/2021
fix: read lean version from the leanpkg.toml file so that installation from elan is set to install the right version from the get go (this avoids duplicate installation of 2 versions during bootstrap).
fix: bring in the LeanPkg service from the old code, updated to new vscode api's with some functionality disabled for now.
fix: issue #57
fix: add reading of Lake style
lean-toolchainfiles to find requested lean version info there.