Lean 4 extension update "Commands & Walkthrough"

Stream: lean4

[Marc Huisinga]

The previously teasered extension features are now ready to be tested!

As these are quite a lot of changes, it would help me a lot if some of you try out the new version of the extension before it is actually released. You can do so by downloading the .vsix-file below, opening the "Extensions" menu in the sidebar, uninstalling your current Lean 4 extension, clicking the icon with three dots at the top and selecting "Install from VSIX...". If you want to go back to the old extension version, simply uninstall the extension and re-install it from the marketplace. If VS Code somehow decides to re-install the version of the extension from the VSIX file, make sure to delete ~/.config/Code/CachedExtensionVSIXs/leanprover.lean4-0.0.113.

lean4-0.0.113.vsix

Bugs and suggestions for improvements are all welcome. If nothing major comes up, I intend to release the new version on 2023-10-22. The code can be found here.

New commands

Creating Projects

Two new commands to create projects have been added: lean4.project.createStandaloneProject and lean4.project.createMathlibProject.

Both commands display a file picker to select the location to create the project at, update Elan before creating the project, create the project using lake init and then run lake update to generate the lake-manifest.json file. Standalone projects use leanprover/lean4:stable for their toolchain; mathlib projects use leanprover-community/mathlib4:lean-toolchain.

After creating a mathlib project, lake exe cache get is called.

When the project is fully initialized, users are prompted whether they want to open the newly created project.

1_NewProject.png
2_NewProject.png

Opening Projects

Two new commands to open existing projects have been added: lean4.project.open and lean4.project.clone.

lean4.project.open is intended to prevent users from accidentally opening the wrong folder. It displays a file picker and then checks if the selected folder is a valid Lean 4 project. The heuristic used here is the same as the one that has been used in the extension so far: If it contains a lean-toolchain file it is a valid Lean 4 project. If it contains LICENSE and LICENSES files, as well as a src folder, it is assumed to be Lean 4 itself and can also be opened with the command.
If the selected folder is not a valid Lean 4 project, the command looks through parent folders to see if it can find one there. If it finds one, it suggests to open that one instead.

lean4.project.clone shows an input that allows users to input a URL to a Git repository. Afterwards, a file picker is opened to select the folder to clone the project to. Then, it clones the project using git clone, attempts to fetch the mathlib cache using lake exe cache get (failing silently if the command is not available) and asks whether the new project should be opened.

1_Open.png
2_Open.png
3_Clone.png

Lake Commands

Four new commands for common Lake operations have been added: lean4.project.build, lean4.project.clean, lean4.project.updateDependency and lean4.project.fetchCache. All of these commands can interfere with the language server, so the Lean client is automatically stopped before running the command and automatically restarted afterwards.

lean4.project.build fetches the mathlib cache if it is available and runs lake build afterwards.

lean4.project.clean displays a confirmation prompt, runs lake clean and then asks the user whether they want to immediately fetch the mathlib cache if lake exe cache is available.

lean4.project.fetchCache simply fetches the mathlib cache if lake exe cache is available.

lean4.updateDependency parses the manifest.json of the project that is currently selected and fetches the current remote revision for each by calling git ls-remote with the input revision designated in the manifest. Dependencies that are still up-to-date are filtered. Then, a selection dialog is displayed to choose the dependency to update, what revision it is currently on and which one it will be updated to.
After selecting a dependency, if the project is a GitHub project, the current remote lean-toolchain is automatically determined. If it differs from the current lean-toolchain of the project, a prompt is displayed, asking the user if they want to update their lean-toolchain to the remote version. If the project is not a GitHub project, users are asked whether they want to continue with updating the dependency without also updating the toolchain version.
Finally, the new toolchain version is written, lake update is called to update the selected dependency and the mathlib cache is fetched if lake exe cache is available.

1_Clean.png
2_Dependencies.png
3_Dependencies.png

Elan

The command to install elan that used to be only accessible by opening a new Lean 4 file without having Lean installed has also been exposed as a command lean4.setup.installElan now.

Command Menu

In the top right, a new menu with the ∀-quantifier from Lean's logo as an icon has been added. The menu provides access to all user-facing commands that the VS Code extension provides.

Since the menu can be used to open and create projects, as well as access documentation related to Lean, it is always displayed, even if no Lean 4 project is open. If one finds this annoying, it can be disabled with a new configuration setting. Certain commands are however only displayed when a Lean 4 file is open, e.g. building the project, as we need a file to determine the project that is currently active in multi-root workspaces.

1_Menu.png

Walkthrough

When the extension is first installed, a platform-specific walkthrough guide is opened that provides information on the following:

• Learning Lean: Links to books, the natural number game and documentation, as well as which target group each resource is intended for.
• Installing dependencies: A short platform-specific guide to get users set-up with Git and curl.
• Installing Elan: A button to install Elan from the walkthrough.
• Projects: A list of buttons that can be pressed to create a new project or obtain an existing one using the aforementioned commands.
• Zulip: An invitation to the Lean Zulip, a short introduction on how to post there and how to post helpful code examples.

The walkthrough can always be re-opened through the "Documentation" submenu in the command menu.

1_Walkthrough.png
2_Walkthrough.png
3_Walkthrough.png
4_Walkthrough.png
5_Walkthrough.png
6_Walkthrough.png

Safeguards

If users accidentally open a folder that is not a Lean 4 project using VS Code's regular "Open Folder" command and then open a Lean file within it, a notification suggesting that a wrong folder has been opened is displayed. If there is a parent folder that is a valid Lean 4 project, the notification suggests to open that folder instead.

If users open a single Lean 4 file, a notification is displayed informing them that not all features are available in this mode and that they should open a project instead.

Both notifications can be disabled with a new configuration setting.

1_Safeguards.png
2_Safeguards.png
3_Safeguards.png

Other Usability Improvements

1. When selecting to restart the server, a confirmation prompt is displayed beforehand.
2. A progress bar is displayed while starting the language server.
3. All expensive external commands now display a progress bar.
4. The progress bar notification now always contains a link to open the output channel where all command output is dumped for troubleshooting purposes.
5. When errors are displayed for any external commands, a button is now displayed to open the command output.
6. All external commands for which a progress bar is displayed can be cancelled by pressing the "Cancel" button on the progress notification. Doing so will terminate the command process.
7. The output channel now also displays the external commands that have been invoked, not just their output.
8. The "Restart File" command can now be activated using the context menu by right clicking in a file.
9. The extension does not ask to install Lean on markdown files anymore.

1_StartClientProgress.png
2_CommandProgress.png
3_ShowOutput.png
4_Output.png
5_RestartContext.png

[Shreyas Srinivas]

Perhaps the installation and testing process could be simplified with a pre-release : https://code.visualstudio.com/api/working-with-extensions/publishing-extension#prerelease-extensions

[Patrick Massot]

Thanks a lot for all this work Marc, it's wonderful!

[Marc Huisinga]

Shreyas Srinivas said:

Perhaps the installation and testing process could be simplified with a pre-release : https://code.visualstudio.com/api/working-with-extensions/publishing-extension#prerelease-extensions

Yes. I wanted to get this out quickly so I just built the vsix and didn't adjust our release script to also allow using pre-releases. Next time :)

[Patrick Massot]

I think a crucial difficulty with hiding everything behind a graphical interface is error handling. You should make sure to find out what happens if you pull off the internet cable or electric power in the middle of any of those operations, and then find some to test them from a country censoring part of internet, and many people using all sorts of Windows antiviruses software trying very hard to prevent users from using their computers.

[Marc Huisinga]

Patrick Massot said:

I think a crucial difficulty with hiding everything behind a graphical interface is error handling. You should make sure to find out what happens if you pull off the internet cable or electric power in the middle of any of those operations, and then find some to test them from a country censoring part of internet, and many people using all sorts of Windows antiviruses software trying very hard to prevent users from using their computers.

All command output is dumped to the Lean: Editor output channel, which can be opened by pressing the respective button if there is an error or even while running the command. See the following screenshots from above:
2_CommandProgress.png
3_ShowOutput.png
4_Output.png

[Marc Huisinga]

But I agree that error reporting for common specific errors could still be improved vs. the command output.

[Patrick Massot]

Having a way to detect that an antivirus is interfering and suggesting to switch it off would be a huge improvement for students using Windows.

[Marc Huisinga]

I'm not sure if this in particular is easy to detect, but feel free to create an issue for it.

[Shreyas Srinivas]

I am guessing this depends on what the antivirus does in particular that makes students suffer. An anti virus is typically written in a way that makes it hard to detect or easy to delete in any way other than through the providers' solution. This is so that malware can't do the same. "Easy" is the keyword here.

That being said, if as an example it is simply blocking access to or downloads from specific sets of URLs, then testing access to them through fake pings might partially help. Antivirus or not, the extension needs to be able to download toolchains and caches from the respective URLs.

[Patrick Massot]

I have no idea how this all works, I'm not using a user-hostile OS. I simply see people struggling and being utterly confused until they switch off their antivirus, or somehow white-list lake.

[Shreyas Srinivas]

I get it. Been there done that. The key thing to remember is that antivirus software often behaves like the malware it is defending from, so solutions won't be easy or foolproof.

[Shreyas Srinivas]

@Marc Huisinga : shall I raise an issue and do a PR over the weekend? The idea is to check access (through lake perhaps?) to a list of URLs and if denied, then send a notification that "the lean 4 extension cannot reach the URLs (see output log) to perform <so and so> operation. Please make sure that you are connected to the internet and have disabled your antivirus"? This then check is then triggered whenever a command that requires the internet is run.

[Marc Huisinga]

Before developing anything, I think a good first step would be to test common anti virus applications and note down how they make the various features of the extension fail (especially with the .vsix above). It may already be possible to provide better error messages purely based on the stderr / error codes of the commands.

[Marc Huisinga]

In some cases, the right place to add the error message may also be in the command itself.

[Shreyas Srinivas]

My suspicion is that testing even common antivirus software for common failures will be a tall order, and worse, it will have to be repeated periodically as the software changes. There are specific interactions which they interfere with, such as lake making calls to specific (URLs) or accessing some directory (such as ~/.cache). Even if we could give users a heads up that their network connection or firewall might be causing trouble, Patrick's students wouldn't get stuck.

[Shreyas Srinivas]

Maybe we could link to a doc page online where we collect common antivirus related problems and fixes.

[Joe Hendrix]

Is there a particular antivirus that is causing these problems? It may be possible to get the AV to adjust it's behavior. It could also be useful to put the file in question on virustotal to see if other AVs flag it.

[Utensil Song]

There are at least 5 scenarios:

1. antivirus intercepts certain network connection activities, like for a domain that has not been authorized yet
2. antivirus intercepts executing certain process that's not authorized, like lake
3. more subtly, antivirus intercepts certain authorized process to initiates external network connections, like lake could be allowed to execute, but it requires extra authorization to connect to network
4. certain domains or IPs can't be accessed without a proxy from the user's internet environment
5. accessing or writing to certain directories is not permitted

These scenarios are brittle and difficult to adjust beforehand, and possibly subjected to corporate or regional policies.

They are all "detectable" from what the Lean tool is trying to do and fail. These scenarios are frustrating for users because a Lean tool could depend on multiple commands and multiple domains to work, and the dependency could be in any steps, and even just one of these commands or domains startle the antivirus, a whole smooth process is interrupted.

In some cases, the right place to add the error message may also be in the command itself.

Indeed, but the guide to fix the issue isn't. A general solution to this might be checking the error output for network/command execution/file access patterns, then provide a general troubleshooting guide for the specific command/domain to succeed.

That said, while it's feasible, it's not really very productive to do, a general troubleshooting guide is probably sufficient.

[Eric Wieser]

Note we already have some troubleshooting info here: https://leanprover-community.github.io/install/project.html#initializesecuritycontext-error-on-windows

[Eric Wieser]

Detecting InitializeSecurityContext in the stdout and pointing to that webpage would be the low-hanging fruit

[Marc Huisinga]

My suspicion is that testing even common antivirus software for common failures will be a tall order

I don't think we can provide concrete helpful error messages for anti virus applications without testing against them. The broad alternative is to suggest checking the internet connection and antivirus on failure when calling any command that installs anything, accesses remote URLs or certain directories, but I believe that this will be quite unnecessarily noisy.

It's not like we need perfect anti virus error reporting, it's perfectly acceptable when the ones that cause the most trouble are covered.

it will have to be repeated periodically as the software changes

I would hope that we can resolve new common ones as they come up with students.

[Eric Wieser]

Patrick Massot said:

I have no idea how this all works, I'm not using a user-hostile OS. I simply see people struggling and being utterly confused until they switch off their antivirus, or somehow white-list lake.

Arguably the problem is the user-hostile manufacturers who sideload nasty AV software on windows machines out of the box. Windows defender doesn't break Lean (though it does massively slow it down until you tell it to stop doing so)

[Eric Wieser]

At LFTCM I think no two users having trouble had the same antivirus

[Shreyas Srinivas]

The broad alternative is to suggest checking the internet connection and antivirus on failure when calling any command that installs anything, accesses remote URLs or certain directories, but I believe that this will be quite unnecessarily noisy.

This is my suggestion. I don't think it is noisy to give error messages when the command is not going to do its job anyway.

[Marc Huisinga]

Eric Wieser said:

At LFTCM I think no two users having trouble had the same antivirus

Did they have trouble with the same commands and how did the issues manifest exactly?

Shreyas Srinivas said:

The broad alternative is to suggest checking the internet connection and antivirus on failure when calling any command that installs anything, accesses remote URLs or certain directories, but I believe that this will be quite unnecessarily noisy.

This is my suggestion. I don't think it is noisy to give error messages when the command is not going to do its job anyway.

I think it may be OK if we link or include a general troubleshooting guide that goes beyond anti virus applications on errors.

[Utensil Song]

Anyway, I guess maybe the antivirus discussion could be moved to a new topic, the new extension experience is overall very nice and smooth, particularly the top-right corner Lean menu (even wish for a bigger button or a whole toolbar).

[Shreyas Srinivas]

I think it may be OK if we link or include a general troubleshooting guide that goes beyond anti virus applications on errors.

That webpage Eric showed or maybe a separate page that documents common painpoints and solutions?

[Utensil Song]

One issue is that I'm using Cursor (an AI-based VS Codium variant) so I can't open walkthrough in it (I have switched back to VS Code to try it out):

image.png

[Marc Huisinga]

Shreyas Srinivas said:

I think it may be OK if we link or include a general troubleshooting guide that goes beyond anti virus applications on errors.

That webpage Eric showed or maybe a separate page that documents common painpoints and solutions?

The leanprover-community page only covers a single error, and I think I would prefer also including it locally in the extension somehow so that loading the troubleshooting guide itself does not require opening a URL (e.g. using custom webview content).

In general, I'm not sure which kinds of errors are common with new Lean users, so I'd appreciate any help from people who often interact with new users in collecting common problems.

[Eric Wieser]

The AV errors I saw at LftCM were either:

• That error, which is when the AV is MitM-ing curl's SSL connection, and curl doesn't like it
• Very high CPU usage due to the AV analyzing every single olean file that Lean opens.

[Utensil Song]

Shreyas Srinivas said:

I think it may be OK if we link or include a general troubleshooting guide that goes beyond anti virus applications on errors.

That webpage Eric showed or maybe a separate page that documents common painpoints and solutions?

It's really just one of a million errors I've seen. It just happened to be documented. And the real cause, per my understanding, is that the (corperate or antivirus) proxy is doing something similar to the man-in-the-middle attack, using a self-signed certificate to monitor the HTTPS traffic, which can be made to be trusted by many applications, just it's not configured for curl . One thing for sure is that this is a network issue, so the "an antivirus program that scans each downloaded file" probably is just a guess and not related ( but related to the CPU slowdown @Eric Wieser mentioned).

[Kevin Buzzard]

Marc Huisinga said:

But I agree that error reporting for common specific errors could still be improved vs. the command output.

I suspect that we will just run into these situations organically, we'll find new users who are confused and will learn what works to unconfuse them.

[Shreyas Srinivas]

While a proper AV-issue specific message would be great, I think we should at least add the stop gap measure of checking network/file access for relevant commands and asking users to turn off their AV/firewall. This would not necessarily hinder the development of better error detection in the long run, and would greatly help new users in the immediate future

[Shreyas Srinivas]

Adding a web link (or even a link to open the page in the documentation viewer) to a page with common fixes improves this stopgap

[Marc Huisinga]

Shreyas Srinivas said:

While a proper AV-issue specific message would be great, I think we should at least add the stop gap measure of checking network/file access for relevant commands and asking users to turn off their AV/firewall. This would not necessarily hinder the development of better error detection in the long run, and would greatly help new users in the immediate future

Just to be sure: You're suggesting that we should provide better errors in the form of a troubleshooting guide when we run the commands, not that we should predict all the different ways in which commands may access resources and provide errors before we run the command, right?

[Shreyas Srinivas]

Yes

[Shreyas Srinivas]

And this is also what I wanted to PR

[Marc Huisinga]

From your previous messages, it sounded like you wanted to send fake-pings before running the command, which is why I was confused.

[Marc Huisinga]

If you want to write the troubleshooting guide covering several common AV or internet connectivity issues and add a button to command error messages to display it, I would gladly review the PR.

[Shreyas Srinivas]

My initial idea was to write a "checkAccess" function. But later I realised that the extension would throw error notifications anyway, and currently all we need is a link to a webpage with common issues+fixes

[Shreyas Srinivas]

Do I have the rights to PR to the vscode extension. I recall that an invite was needed for mathlib

[Ruben Van de Velde]

I think you can create a fork of your own and create a pr from there

[Joachim Breitner]

From the description it seems that the extension's commands, for example update dependencies, performs steps that the underlying tools do not do (handling toolchain files), or at least do not do yet. I guess a bit of competition between the CLI and the GUI tooling is healthy?

[Utensil Song]

CLI ultimately determines the upperbound of user experience. If a CLI is fragile to any unexpected situation and silent or even misguided about where went wrong, GUI can do only so much bandage. GUI wraps the normal process nice and smooth, yet the user is dropped to the wild to survive if something derails even a little. I saw there are some discussions about CLI vs GUI, like where an issue should be better fixed, I would argue that they all should be fixed at the source (i.e. CLI) eventually. If GUI is doing more steps, it clearly indicates something to be improved on the end of CLI (or the program).

[Shreyas Srinivas]

Utensil : Agreed, specifically with the word eventually. But the changes being proposed are in lake and they are not going to happen right away. This has been discussed before, but the reason GUI changes are proposed is threefold:

1. Not load lake with a bunch of shortcut behaviours that will have to be taken into account as lake's dependency and version management get better. It is hard to build a proper dependency management tool even without having such considerations.
2. Provide UX functionality where it truly belongs. CLIs are always going to have footguns, because their target audience is the power user who demands flexibility. GUIs provide carefully crafted features for those who don't want to touch the CLI.
3. Many feature requests here are specific to mathlib users and need to be met on a more immediate basis. For example math professors teaching students who are new to it all. Most such users are not CLI users.

As lake eventually stabilises, the machinery under the GUI can be adapted in such a way that non CLI users never notice anything. Until then new CLI-averse users need a set of safe options.

[Utensil Song]

Yes, totally agree. It's definitely great to have GUI evolve faster and more flexible and responsive to the need of end users, and keep normal usage as far as possible from footguns. It's also a testbed and part of the feedback loop of how underlying implementation could evolve towards.

[Miguel Marco]

I have given a quick try and it looks great.

Any chance that the extension could also take care of installing the dependencies (git/curl)?

[Marc Huisinga]

On Windows, this is somewhat difficult. I believe that on newer versions of Windows 10, winget is available by default and can install git, though.
For Linux, I suppose we could try a bunch of common package managers to install dependencies, though I expect this to be controversial.
Not sure about Mac, as I'm not a Mac user. It would be nice to get feedback from Mac users on whether the installation procedure suggested in the walkthrough is reasonable.

[Shreyas Srinivas]

Marc Huisinga said:

If you want to write the troubleshooting guide covering several common AV or internet connectivity issues and add a button to command error messages to display it, I would gladly review the PR.

As step 1 for this, I have opened a PR on the leanprover community website repository. I am trying to get the PR reviewed and crowd source some initial issues + fixes. I have created a thread for collecting these issues.

[Shreyas Srinivas]

It's under #general >Troubleshooting Page

[Shreyas Srinivas]

I welcome any suggestions and issues so that I can add them to the page.

[Shreyas Srinivas]

About macOS: If the system has homebrew installed, then then installing git is feasible. If the system has xcode installed (which is not unlikely) then every xcode update can potentially mess up the installation. Asking mac users not to install xcode is a big deal since it is an awesome IDE and comes with a lot of other programming utilities.The other question is whether lean's extension should be doing such things as installing an entire package manager. curl is going to be already part of the system.

[Sebastian Ullrich]

@Shreyas Srinivas I don't know much about macOS, what parts can be messed up by an xcode update?

[Sebastian Ullrich]

(I don't recall any complaints about git from macOS users so far, or Linux for that matter)

[Shreyas Srinivas]

Until earlier this year, every time xcode got updated you had to run some xcode-select --install to get access to git again (among other CLI commands)

[Shreyas Srinivas]

This would happen each time Mac ran system updates that affected xcode.

[Patrick Massot]

I know it's a bit cray, but how hard would it be to ship Lean with enough of git to make this work?

[Henrik Böving]

Git does have a few requirements like perl, OpenSSH, some SSL library that we should really not ship ourselves IMHO. So that rules it out for UNIX style platforms already. I don't know exaclty how the git for windows fork works but I can't imagine it's much better.

[Sebastian Ullrich]

@Patrick Massot If by "this" you mean fetching dependencies like mathlib, it's something I've been thinking about before - especially as getting an http archive from GitHub can actually be faster than using git. But that would only get you as far as "now I actually want to share my code with others", so the cost/benefit ratio is not clear.

[Patrick Massot]

I have no idea how software distribution work on OSes that have no package manager. But git is de facto a dependency of Lean. How do other software manage dependencies on Windows?

[Patrick Massot]

On Linux the model is clear: there should be packages providing elan the normal way (deb, rpm...) with git as a dependency.

[Henrik Böving]

Patrick Massot said:

I have no idea how software distribution work on OSes that have no package manager. But git is de facto a dependency of Lean. How do other software manage dependencies on Windows?

It is sadly very common to just package up all of the libraries that you need into your installation archive and ship them. But this can easily lead to people using outdated and potentially vulnerable libraries unless you basically force them to update, at which point we are just emulating our own package management.

[Patrick Massot]

That was my guess. So indeed it is sad but seems to be the only was to provide the UX that people using Windows or MacOS expect.

[Shreyas Srinivas]

Here is a non-official list of xcode CLI tools @Sebastian Ullrich . All these tools can be affected by the xcode developers making inconvenient decisions, If we want a macOS installer for git

[Sebastian Ullrich]

I think xcode users breaking their git is the user group I'm least concerned about. They should be interested in fixing it anyway, and they will probably figure out how to.

[Patrick Massot]

@Marc Huisinga in the new extension, is there a command to update Mathlib (either when working on Mathlib or on a project depending on it)?

[Patrick Massot]

Now I see it. I think the extension was in a weird state.

[Shreyas Srinivas]

Sebastian Ullrich said:

I think xcode users breaking their git is the user group I'm least concerned about. They should be interested in fixing it anyway, and they will probably figure out how to.

Xcode is the standard way to install and run these CLI tools. AFAIK, brew packages use the xcode CLI too. This is why I brought it up. There are ways to circumvent xcode, but MacOS goes out of its way to make life painful for external installers.

[Shreyas Srinivas]

You'll get an error about "invalid developer path" or something similar

[Shreyas Srinivas]

If you are a student who is doing some programming as well as math and lean, it is unlikely that you won't install the xcode CLT.

[Marc Huisinga]

Patrick Massot said:

Now I see it. I think the extension was in a weird state.

One possible thing that may be confusing you: Project actions and such are only displayed when the editor language is lean 4, i.e. when you're focussing a Lean 4 editor tab. I have plans to improve this in the future but it's all a bit annoying, so not in this version yet.

[Patrick Massot]

You menu the ∀ menu is there but it contains less items?

[Patrick Massot]

That would indeed explain my confusion.

[Patrick Massot]

I also realize another source of confusion is that the ∀ menu is displayed in the upper right corner of the currently active panel and not the upper-right corner of VSCode. So it frequently jumps from the editing panel to the infoview panel. But I fear this is a problem with VSCode itself.

[Marc Huisinga]

Patrick Massot said:

You menu the ∀ menu is there but it contains less items?

Yes. There are items that are always enabled (opening projects, documentation, etc) and items that are only enabled when we can be sure that we're actually in a Lean 4 context.

[Marc Huisinga]

That said, I'm aware that this is not optimal and it will be improved in the future.

[Patrick Massot]

I just tried creating a new Lean project ( depending on Mathlib) and VSCode is completely confused between Lean 3 and Lean 4.

[Patrick Massot]

image.png

[Marc Huisinga]

Interesting. You probably have both extensions installed, right? I'll see if I can fix that tomorrow.

[Patrick Massot]

I have both the Lean 3 extension and your Lean 4 one.

[Miguel Marco]

I wouldn't worry about linux users (or at least, i would put them on the least priority queue). They are used to instructions that involve running some script in a terminal.

My worry is mostly about windows and mac users.

One more question: I remember seeing an option in the older extension about allowing it to manage elan. Has it dissapeared?

[Shreyas Srinivas]

Miguel Marco said:

My worry is mostly about windows and mac users.

macOS won't be easy since they push xcode clt everywhere and this easily messes with other installs (although installing xcode is trivial from the app store). That being said, git offers its GUI installer for both Mac and Windows.

[Shreyas Srinivas]

Once you have git installed, there are very good git extensions on vscode that already do a splendid job of keeping the CLI away, over and above vscode's inbuilt git integration.

[Scott Morrison]

I have never experienced this supposed problem with git and xcode, in many years of using both git and xcode.

[Scott Morrison]

which git reports /opt/homebrew/bin/git

[Utensil Song]

The only problem on Mac M1 I have is VS Code Extension can't install elan, I need to figure out that it's actually as simple as brew install elan-init which indicates the binary exists but provided not by elan and VS Code extension hasn't handled such subtleties yet. But I guess it should be addressed from the elan script end?

I have encountered the git issue once or twice, but it resolved really quick, so I have not much impression, the confusing part I recalled was that it hangs in the terminal then pops out the GUI prompt in the first screen instead of the terminal screen, so I have to notice it only when I went back to the first screen (trying to figure out if the problem is network related).

[Utensil Song]

You can see that the drastic drop of experience comes from being dragged to the other UI world:

• when you are using GUI and suddenly you have to figure out what went wrong on the CLI end,
• or you are happily enjoying CLI (or a script/program) on the terminal, and suddenly a GUI blocks it (there are more examples, like login credential helpers, and like first time accessing some file system location from terminal). Another example is apt/rustup/elan and many installers are interactive by default, and one has to supply -s -- -y like stuff to make them work.

[Utensil Song]

I seldom use Linux GUI nowadays, mostly I access Linux from terminal or a Web UI, the former gives me total control, and the latter gives me modern experience (i.e. Codespaces or VS Code server or plain docker for working with Lean).

On Windows, I've fought with many generations of OS/AV or "security" policies, became fluent and lost count. It's always a half-baked and restricted world for developers, and the bundle-all one-click install packs are unfortunately the quickest way to get to the real work, so for a rapid involving area like lean (or e.g. LLM), I would avoid using Windows most of the time, or I'll have to going over the setup tweaks frequently, which eats my limited time for the real work.

[Shreyas Srinivas]

@Scott Morrison : I just found a stackexchange thread about this

[Patrick Massot]

@Marc Huisinga I think the message
image.png
misses some explanation, or at least the world toolchain (or Lean version).

[Marc Huisinga]

Patrick Massot said:

Marc Huisinga I think the message
image.png
misses some explanation, or at least the world toolchain (or Lean version).

You're right, I think it should be clearer that we're updating the version of the project, not something else.

[Patrick Massot]

Maybe I read the message too quickly, but my first reaction was it is not clear enough for beginners.

[Patrick Massot]

And then after closing this message and waiting, there is a message saying "Imports are out of date and must be rebuilt; use the "Restart File" command in your editor.". I guess it comes directly from lake and tries to be editor agnostic, but the result is that VSCode using beginners won't know where is the restart file command.

[Shreyas Srinivas]

Shreyas Srinivas said:

Marc Huisinga said:

If you want to write the troubleshooting guide covering several common AV or internet connectivity issues and add a button to command error messages to display it, I would gladly review the PR.

As step 1 for this, I have opened a PR on the leanprover community website repository. I am trying to get the PR reviewed and crowd source some initial issues + fixes. I have created a thread for collecting these issues.

After discussing this in the #general > troubleshooting page topic, I have raised an RFC issue on the lean 4 repo to add this page to the lean manual. If you consider this issue important, it apparently helps if you add a :like: to the issue. Here's the issue: https://github.com/leanprover/lean4/issues/2698

The PR to add the page will follow once I get approval on the issue. The addition of the troubleshooting link to vscode error messages will follow once we have the troubleshooting page.

[Shreyas Srinivas]

I am guessing the last part will also have to follow the "make an RFC issue" step and then the "raise a PR" step.

[Marc Huisinga]

I've incorporated some of Patrick's comments:

• As soon as the extension activates all of its Lean 4 specific features (e.g. the infoview) after opening a Lean 4 file once, the menu will always contain all entries, so it should be less confusing. If an entry cannot be used in a specific situation, the extension will report back with an error.
• Fix the Lean 3 / Lean 4 confusion issue.
• Hopefully make the toolchain update message less confusing.

You can now try this new version before it is released to everyone using a VS Code pre-release by clicking the following button in the Extensions sidebar menu in VS Code:
image.png

Specifically, there is now no need to manually install a .vsix file for testing anymore.

[Patrick Massot]

Thanks!

[Patrick Massot]

FYI, I just tried updating an ancient project using the new extension and it totally failed. That project was a bit more than one year old, hence it didn't include a lake-manifest.json. I think it doesn't make sense to invest a lot of time supporting this, but I thought I would report this anyway.

[Marc Huisinga]

Patrick Massot said:

FYI, I just tried updating an ancient project using the new extension and it totally failed. That project was a bit more than one year old, hence it didn't include a lake-manifest.json. I think it doesn't make sense to invest a lot of time supporting this, but I thought I would report this anyway.

If the failure includes any of the new commands, that's to be expected.
My current policy is to support all Lean 4 versions from the first stable release onwards for new features, and to not break backwards compatibility for existing features with Lean 4 versions that are less than one year old, including versions pre-stable. Were the pre-update features (e.g. infoview, restart file, etc) still functional in that old project?

[Patrick Massot]

Yes, only the new stuff seems broken.

[Patrick Massot]

If you are curious and want to experiment, this is a public project: https://github.com/PatrickMassot/verbose-lean4

[Utensil Song]

When upgrading old Lean 4 projects, it seems to just start over with the meta (tool-chain, lakefile etc.) and incorporate existing contents, usually I have to lake new a new project structure elsewhere then copy things over because lake new doesn't allow override.

Maybe the extension can do something similar, like detecting the project doesn't even meet the minimal support criteria, then prompt the user to upgrade it completely, then do a lake new override?

[Peter Nelson]

Is it too late to request a 'paste tactic suggestion' feature like the lean 3 extension had?

[Utensil Song]

This is already supported if you click the tactic suggestion in widgets, it would replace the current tactic.

[Marc Huisinga]

Utensil Song said:

When upgrading old Lean 4 projects, it seems to just start over with the meta (tool-chain, lakefile etc.) and incorporate existing contents, usually I have to lake new a new project structure elsewhere then copy things over because lake new doesn't allow override.

Maybe the extension can do something similar, like detecting the project doesn't even meet the minimal support criteria, then prompt the user to upgrade it completely, then do a lake new override?

I think the benefit of this will diminish considerably over time.

[Peter Nelson]

Utensil Song said:

This is already supported if you click the tactic suggestion in widgets, it would replace the current tactic.

Yes, but the lean3 version had a keyboard shortcut.

[Utensil Song]

Ah, that might be tricky. Did it work for multiple tactic suggestions?

[Peter Nelson]

I don't think I ever tried - but for me the main use was squeeze_simp, after typing which one could press [keyboard shortcut] and have the suggestion appear in the editor. Being able to do this for simp? would be fantastic.

[Mauricio Collares]

Shift-Alt-. or Ctrl-. should work on VS Code, and C-l a a should work on vanilla emacs

[Mauricio Collares]

(deleted)

[Peter Nelson]

Thanks - but I can't figure out the equivalent on vscode mac

[Mauricio Collares]

Maybe ⌘-.? According to https://code.visualstudio.com/shortcuts/keyboard-shortcuts-macos.pdf at least

[Peter Nelson]

Thanks!

[Marc Huisinga]

This has been released to everyone now.

[Shreyas Srinivas]

I don't see a separate project menu, but I can see the commands in the palette.

[Marc Huisinga]

Shreyas Srinivas said:

I don't see a separate project menu, but I can see the commands in the palette.

Open a file. The title bar menu is unfortunately only displayed when any file has been opened.

[Shreyas Srinivas]

I am in a lake project

[Shreyas Srinivas]

For good measure, I closed all vscode windows and restarted them (although this is usually not necessary). Same result.

[Shreyas Srinivas]

Might I suggest that the menu be called Lean instead of Project which is very generic (it still isn't showing up)?

[Eric Wieser]

Marc Huisinga said:

Open a file. The title bar menu is unfortunately only displayed when any file has been opened.

I think this is probably an indication that we are mis-using the file-level toolbar, since many of the operations there do not operate on a file level

[Eric Wieser]

(perfection is the enemy of the good and all that, so I'm glad we have a menu somewhere; but I'm unconvinced that this is the right long-term home for it)

[Marc Huisinga]

Eric Wieser said:

(perfection is the enemy of the good and all that, so I'm glad we have a menu somewhere; but I'm unconvinced that this is the right long-term home for it)

Unfortunately, VS Code does not let us contribute to the "right place" for this kind of menu. The only alternative that extensions are allowed to use is a sidebar menu (also called "views" because they're really intended for UIs, not lists of commands), which is somewhat inconvenient because you have to open it and close it again after calling a command.

[Marc Huisinga]

See https://code.visualstudio.com/api/references/contribution-points

[Eric Wieser]

It looks like you can contribute to the top-level menu alongside "file"

[Marc Huisinga]

Eric Wieser said:

It looks like you can contribute to the top-level menu alongside "file"

With which contribution point?

[Eric Wieser]

Hmm, I now seem to have lost it. Does explorer/title in contributes.menus work?

[Marc Huisinga]

explorer/title is the three dot menu in the explorer sidebar menu, I think

[Eric Wieser]

It seems it's not supported anyway: https://github.com/microsoft/vscode/issues/108271

[Shreyas Srinivas]

Could there be a menu on the sidebar instead? like latex-workshop?

[Eric Wieser]

Here's how to contribute to the explorer menu: https://github.com/eamodio/vscode-toggle-excluded-files/blob/98a87df11afcbd5cb7b9ba23d9704ccbcda376a2/package.json#L138-L150

[Eric Wieser]

That extension adds this center button:

image.png

[Marc Huisinga]

Eric Wieser said:

That extension adds this center button:

image.png

The problem with the explorer menu bar is that it's even more difficult to find than the editor title bar. For the latter you need to open a file, for the former you need to open the right sidebar and then hover your mouse over the explorer sidebar so that the icon is displayed.

[Marc Huisinga]

... And if you somehow happen to collapse the Mathlib4 menu, the icon just disappears altogether

[Shreyas Srinivas]

Can't we add an icon on the activity bar? once we click on it the extension gets running.

[Shreyas Srinivas]

The activity bar is always visible by default

[Marc Huisinga]

The activity bar / sidebar contributes views. See a few posts above for why I did not implement a view.

[Mario Carneiro]

I just got the new version of the extension, and while I'm still discovering new things, one thing that I'm not a fan of is that my number 1 most triggered command "Lean 4: Server: Restart Server" which I have bound to a key command now has an "are you sure you want to restart" dialog which shows up every time. I don't see a need for this, the server is not stateful so the worst consequence of restarting is having to wait for it to get back to your current position

[Marc Huisinga]

Mario Carneiro said:

I just got the new version of the extension, and while I'm still discovering new things, one thing that I'm not a fan of is that my number 1 most triggered command "Lean 4: Server: Restart Server" which I have bound to a key command now has an "are you sure you want to restart" dialog which shows up every time. I don't see a need for this, the server is not stateful so the worst consequence of restarting is having to wait for it to get back to your current position

Hmmm, I think I agree in hindsight and I doubted myself over whether it's a good idea a couple of times, but since nobody commented on it during the testing phase, I figured that it will be alright. I can remove it again if nobody objects that it should stay.

[Sebastian Ullrich]

@Mario Carneiro I would agree that there is no need for the dialog but I'm still curious: why are you restarting the server that often, more often than the file workers?

[Mario Carneiro]

It may just be force of habit, but when there is corrupt state or other weird debugging stuff it's easier to be sure that restarting the server gets me into a known state

[Mario Carneiro]

I will use refresh file dependencies when actually leaning normally

[Patrick Massot]

This morning I tried to get students using the new version of the extension. But one student had VSCode refusing to upgrade the extension. He would briefly see version 0.0.117 but then after a couple of seconds it rolled back to 0.0.113. He uses macOS version: Ventura 13.2.1. Any idea what could be causing this?

[Marc Huisinga]

One possibility is that their VS Code version is old somehow. The extension update bumped the required VS Code version from 1.70.0 (released in July 2022) to 1.75.0 (released in January 2023).

[Marc Huisinga]

Alternatively, they can also try to uninstall the extension, close VS Code, delete all occurrences of leanprover.lean4-0.0.113 in the home folder and then restart and reinstall the extension. I'm not sure where VS Code caches extensions on MacOS, but it should be somewhere in the home folder.

[Patrick Massot]

I tried closing VSCode and removing the $HOME/.vscode. I will check the VSCode version. The student should come to my office later today to get some help.

[Patrick Massot]

We managed to fix it. Indeed his VSCode was too old. The crazy thing is why it was too old. He downloaded VSCode from the website so MacOS put VSCode in the download folder. But the download folder seems to be read-only for everyone but Safari. So VSCode was not able to auto-update. We moved VSCode to the Applications folder and there it auto-updated and then the Lean extension auto-updated. User-hostile OSes are really crazy...

[Shreyas Srinivas]

Some day in the distant future, when lean can run on wasm, maybe the extension could work on https://vscode.dev/

[Patrick Massot]

@Marc Huisinga how far are your VSCode extension menus from being the official recommended way of installing Lean? I'm asking because some colleagues just asked me how to install Lean. All the documentation I can find still doesn't refer to your menu.

[Marc Huisinga]

A couple of days. I'm working on updating the manual right now.

[Patrick Massot]

Great!

[Miguel Marco]

Marc Huisinga said:

A couple of days. I'm working on updating the manual right now.

You mean it will be possible to install lean+mathlib just within vscode in windows/mac/linux?

[Patrick Massot]

It is already possible (at least when nothing goes wrong). We are discussing the documentation side,