Elan 4.0.0rc1 & Lean 4 VS Code extension pre-release 0.0.187

Stream: lean4

[Marc Huisinga]

A new release candidate for Elan 4.0.0 and a new Lean 4 VS Code extension pre-release version with support for Elan 4.0.0 are now available.

New features in Elan 4.0.0

• Eager toolchain resolution: Release channels like leanprover/lean4:stable or leanprover/lean4:nightly are now resolved to their current version when the corresponding release channel is used, not to the version that is currently installed.
  • This resolves a long-standing usability issue where many users would install leanprover/lean4:stable for their default toolchain when first installing Elan, which meant that commands like lean or lake outside of the scope of a Lean project would always use an old Lean version from when leanprover/lean4:stable was first installed.
  • Eager toolchain resolution requires additional network accesses when using release channels and may also download a new Lean version when a release channel resolves to a version that is not installed. If leanprover/lean4:stable cannot be resolved to a new version (e.g. because there is no internet connection), Elan will fall back to the most recent installed Lean version for that release channel. Additionally, as described below, the Lean 4 VS Code extension now has additional support to control network accesses and downloads by Elan when using it from within VS Code.
• Unused toolchain garbage collection: Elan now supports new commands elan toolchain gc and elan toolchain gc --delete to delete unused toolchains.
  • The garbage collector is only triggered using these commands.
  • A toolchain is considered 'used' by Elan if there is a local project using that toolchain and Elan 4.0.0+ has been used in it without the project being moved to a different filesystem location afterwards.
  • Automation can use elan toolchain gc --json to query information from elan toolchain gc. The format can be found here.
• elan dump-state [--no-net]: This new Elan command can be used by automation to extract information from Elan about toolchains.
  • --no-net will force Elan to not resolve Lean release channels so that information about the current offline state of Elan can be extracted.
  • The format can be found here.

New features in Lean 4 VS Code extension pre-release 0.0.187

With all of these new features enabled by Elan 4.0.0, 0.0.187 of the Lean 4 VS Code extension provides the following new functionality:

• Toolchain download confirmations: For users on a slow network connection or on a limited data plan, it can be quite frustrating that Elan in VS Code will start downloading a new toolchain whenever a project with a non-installed toolchain is accidentally opened. This issue is made more severe by the changes in Elan 4.0.0, as users often use leanprover/lean4:stable for their default toolchain, and so opening a new file in VS Code can initiate a download when a new stable Lean version is released. 0.0.187 resolves this issue by introducing a new 'Always Ask Before Installing Lean Versions' VS Code setting that causes the Lean 4 VS Code extension to prompt users before installing a new Lean toolchain. If users decide not to install the new version, the Lean 4 VS Code extension will either use the most recent installed version for release channels or abort launching the language server otherwise.
  • 'Always Ask Before Installing Lean Versions' is disabled by default to keep the behavior as close as possible to the current behavior. However, when installing or updating Elan using the Lean 4 VS Code extension, it will now display a prompt, asking whether users want to enable this setting.
  • Even when 'Always Ask Before Installing Lean Versions' is disabled, the Lean 4 VS Code extension will still prompt users when opening a file in VS Code will update the toolchain for a release channel like leanprover/lean4:stable. This ensures that the additional automatic downloads induced by eager toolchain resolution of Elan 4.0.0 are always optional in VS Code.
• VS Code command for manually updating the Lean version of a release channel: A new 'Setup: Update Release Channel Lean Version' VS Code command can be used to manually update the Lean version of release channels. This is helpful if you have decided to not update an eagerly resolved Lean version for a release channel in VS Code in the current VS Code session, or if you simply want to update the Lean version of a release channel prematurely, before using the release channel in VS Code.
• VS Code commands for selecting project and default toolchains: New 'Setup: Select Default Lean Version' and 'Project: Select Project Lean Version' VS Code commands can be used to select the default or the project Lean version. Both of these commands display dialogs that allow choosing a toolchain from all available toolchains (queried from https://release.lean-lang.org/), not just the installed ones.
• VS Code command for uninstalling Lean toolchains: A new 'Setup: Uninstall Lean Versions' command can be used to uninstall installed toolchains. This command has support for the new garbage collector in Elan 4.0.0.

Screenshots of new Lean 4 VS Code extension functionality

Toolchain installation confirmation prompt

Release channel update confirmation prompt

New 'Version Management' menu

'Setup: Update Release Channel Lean Version' dialog

'Setup: Select Default Lean Version' dialog

'Setup: Uninstall Lean Versions' dialog

Testing Elan 4.0.0-rc1 and Lean 4 VS Code extension pre-release 0.0.187

All of these new features require significant changes to Elan and the Lean 4 VS Code extension, so we would be very grateful if you could help us test these changes before we release them to everyone.

You can install the Lean 4 VS Code extension pre-release by right-clicking on the Lean 4 extension in the VS Code 'Extensions' menu and selecting 'Switch to Pre-Release Version':

Switching to a pre-release version

0.0.187 is backwards-compatible with older Elan versions, so it should not cause any issues with Elan 3.1.1.

After installing 0.0.187, you can install the Elan 4.0.0 pre-release by downloading the archive for your system from the Elan release page, unpacking it and running the elan-init executable from the archive from the command line. After installing Elan 4.0.0-rc1, Elan will automatically delete some toolchains that use an outdated format from your .elan directory (specific stable and release candidate toolchains will not be removed).

Once both 0.0.187 and Elan 4.0.0-rc1 are installed, you should be ready-to-go. Please report all new issues you encounter here so that we can fix them before releasing Elan 4.0.0 and the corresponding changes to the Lean 4 VS Code extension to everyone. Thanks!

[Shreyas Srinivas]

So does elan track all the local projects started with recent toolchains?

[Shreyas Srinivas]

Does this work for projects cloned from GitHub for instance? Or is it just projects that were created locally?

[Sebastian Ullrich]

It doesn't care about creation, only that you used a Lean toolchain with the project at least once

[Shreyas Srinivas]

Could we put this to use and store Mathlib caches at the toolchain level?

[Shreyas Srinivas]

Currently we have math based project folders which are like 5GB

[Shreyas Srinivas]

Another question: how does elan know that a project that once used a toolchain stopped using it after toolchain updates?

[Sebastian Ullrich]

If you are interested in the implementation, the code shouldn't be too unreadable I hope

[Marc Huisinga]

We are planning to release these changes around 2025-01-30T14:00:00+01:00, so pre-release testing will continue for another week.

[Marc Huisinga]

Both Elan 4.0.0 and 0.0.192 of the Lean 4 VS Code extension have been released. You can update Elan with the 'Setup: Update Elan' command in VS Code after restarting VS Code.

Updating Elan

The Elan 4.0.0 changelog can be found here and the 0.0.192 VS Code extension changelog can be found here.

Please let us know if you encounter any new issues on Elan 4.0.0 or 0.0.192 of the VS Code extension.

Note for tooling developers: Due to eager toolchain resolution in Elan 4.0.0, the elan toolchain update command has been removed, as it is not needed anymore.

[Michael Stoll]

After updating the VS Code extension (which added the menu option "Update Elan") and clicking on "Upadate Elan", I got a pop-up window asking me if I want to be asked before downloading lean versions, which I denied. I then got an error

Unable to write to User Settings because lean4.alwaysAskBeforeInstallingLeanVersions is not a registered configuration.

which I guess means that my answer was not recorded, but otherwise looks harmless...

[Marc Huisinga]

Michael Stoll said:

After updating the VS Code extension (which added the menu option "Update Elan") and clicking on "Upadate Elan", I got a pop-up window asking me if I want to be asked before downloading lean versions, which I denied. I then got an error

Unable to write to User Settings because lean4.alwaysAskBeforeInstallingLeanVersions is not a registered configuration.

which I guess means that my answer was not recorded, but otherwise looks harmless...

Argh. Could you restart VS Code and check if the setting exists by opening the settings menu and pasting that identifier into the search?

[Marc Huisinga]

Also, did you restart VS Code before clicking the "Update Elan" button, or did you just click the "Restart Extensions" button?

[Michael Stoll]

Marc Huisinga said:

Also, did you restart VS Code before clicking the "Update Elan" button, or did you just click the "Restart Extensions" button?

The latter. I can try restarting VS Code, but not now (I have an appointment in one minute...)

[Michael Stoll]

After closing VS Code and starting it again, it does find the relevant setting.

[Marc Huisinga]

Thanks. I suspect what's going on here is that there's a VS Code bug related to the "Restart Extensions" button not correctly dealing with new configuration options. I've changed the description above to suggest a restart before updating Elan.