Lean 4 VS Code extension pre-release 0.0.210

Stream: general

[Marc Huisinga]

A new Lean VS Code extension pre-release is now available (v0.0.210). Notable changes include:

• A new Lean installation procedure that automatically installs Git and curl on most common systems instead of requiring users to install them manually from the terminal (vscode-lean4#641)
• Language server support for lakefile.toml (syntax errors, auto-completion and hovers) via Even Better TOML, which the Lean VS Code extension will now depend on (vscode-lean4#646 and lean4#9871)
• A new sort order of 'All messages' that sorts messages by their proximity to the text cursor, instead of their absolute position in the file (can be changed with a setting) (vscode-lean4#645)
• A recommended minimum Elan version of 4.0.0

The full changelog can be found here.

I'd be very grateful for any help with testing this pre-release before we roll it out to everyone. You can install the pre-release by opening the 'Extensions' side-bar view, clicking the cog icon on the 'Lean 4' extension and selecting 'Switch to Pre-Release Version':
Switching to pre-release

Thanks!

[Marc Huisinga]

This has now been released to everyone as 0.0.212.

If you see anyone running into problems with the new installation procedure, please let me know!