Lean 4 VS Code extension pre-release 0.0.185

Stream: lean4

[Marc Huisinga]

A new Lean 4 VS Code pre-release version is now available. It enables the InfoView to be detached into a separate window on sufficiently recent VS Code versions (e.g. for use on a second monitor), improves the UX of the startup errors that users see when their setup is broken and adds a small spinner to the InfoView to indicate when it is busy loading.

Demo of detachable InfoView

Since these changes also include a larger refactoring, I would be very grateful for some pre-release testing of these changes before they are released to everyone. You can opt-in to pre-release versions of the Lean 4 VS Code extension by right-clicking the 'Lean 4' extension in the 'Extensions' sidebar menu and clicking 'Switch to Pre-Release Version'.

Switching to pre-release versions

The full release notes can be found here.

Please report all regressions you encounter on the pre-release version in this thread so that I can fix them before the final release. Thanks!

[Marc Huisinga]

These changes have now been fully released as part of 0.0.186. Please let me know if you encounter any new problems on this version.