Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: support for elan 4.0.0 #554

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

feat: support for elan 4.0.0 #554

wants to merge 1 commit into from

Conversation

mhuisi
Copy link
Collaborator

@mhuisi mhuisi commented Dec 6, 2024

This PR implements support for Elan 4.0.0. Specifically:

  • A new setting that can be enabled to issue confirmation prompts before installing new toolchains
  • Confirmation prompts before eagerly updating release channels when opening Lean files in VS Code with Elan 4.0.0's eager toolchain resolution
  • New VS Code command integrations for Elan:
    • Project and default toolchain selection that displays all available Lean toolchains by using https://release.lean-lang.org/
    • Toolchain deinstallation, including integration for elan toolchain gc in Elan 4.0.0
    • Manual updates of release channel toolchains

It also fixes a couple of bugs:

  • When the output of elan show got too large, the 'Troubleshooting: Show Setup Information' command would display a dialog that could exceed the height of the screen, hiding all buttons. With Elan 4.0.0, the content of this dialog is now kept much smaller so that this cannot happen on most screens anymore.
  • The InfoView would sometimes report internal errors (including stacktraces) when something went wrong on the VS Code side of the InfoView. Now it correctly displays the error.
  • The order of the buttons in lots of modal dialogs was a bit unorganized, and it should now be more coherent.
  • If the default toolchain was changed while VS Code was running, the VS Code extension would hold on to the old toolchain for the language client of untitled files indefinitely.
  • VS Code extension commands that use the active client of the client provider would behave incorrectly or use an incorrect client if a client failed or was stopped manually using a command.
  • The 'Restart Server' command didn't always restart the setup check for the selected language client if that language client had failed in the past.
Update dialog

Update_Dialog

Installation dialog

Installation_Dialog

New version management commands

New_Version_Management_Menu

Default version dialog

Default_Version_Dialog

Release channel update dialog

Release_Channel_Update_Dialog

Version uninstall dialog

Version_Uninstall_Dialog

This PR will be merged at the start of 2025.

@mhuisi mhuisi force-pushed the mhuisi/eager-elan branch from 60f161d to 66597f2 Compare December 9, 2024 12:07
@mhuisi mhuisi marked this pull request as ready for review December 12, 2024 18:59
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant