Better setup diagnostics in VS Code

Stream: lean4

[Marc Huisinga]

The better setup diagnostics PR was recently merged into vscode-lean4 and has been added to a new pre-release (0.0.145). It adds new warnings and errors to the VS Code extension that are displayed when potential issues are detected with the user's Lean 4 setup and provides a new command ('Troubleshooting: Show Setup Information') to dump all kinds of context information about the user's setup to make it easier to debug setup issues, especially here on Zulip. The details of what exactly is checked by the extension are in the PR description. All warning-level setup notifications can be disabled using the 'Lean4: Show Setup Warnings' setting.

It's possible that the new error-level diagnostics may cause issues for users with exotic Lean 4 setups. If you think that this applies to you (e.g.: Nix users, corporate users, users from China, ...), please read the PR description carefully and install the pre-release as described below. If this PR is causing issues for you, please let me know.

To facilitate these changes, another major rewrite of the VS Code extension was needed. It is likely that it still contains bugs, so I would greatly appreciate if people from the Lean community could help me test it. If you already opted-in to vscode-lean4 pre-releases in the past, you don't need to do anything and VS Code will automatically upgrade to the pre-release. Otherwise, you can opt-in to pre-releases here:
Installing a pre-release

Dumping setup information

Here's an example of the kind of setup information that the 'Troubleshooting: Show Setup Information' command can provide:
'Show Setup Information' command

Operating system: Linux (release: 6.8.8-300.fc40.x86_64)
CPU architecture: x64
CPU model: 8 x Intel(R) Core(TM) i7-10510U CPU @ 1.80GHz
Available RAM: 16.44 GB

Curl installed: true
Git installed: true
Elan: Reasonably up-to-date (version: 3.1.1)
Lean: Reasonably up-to-date (version: 4.7.0)
Project: Valid Lean project (path: /home/mhuisi/Lean4Test16)

---

Elan toolchains:

installed toolchains
--------------------

leanprover/lean4:stable (default)
leanprover/lean4:v4.7.0
leanprover/lean4:v4.8.0-rc1

active toolchain
----------------

leanprover/lean4:v4.7.0 (overridden by '/home/mhuisi/Lean4Test16/lean-toolchain')

Lean (version 4.7.0, x86_64-unknown-linux-gnu, commit 6fce8f7d5cd1, Release)

[Patrick Massot]

I think something is not working. @Marc Huisinga everytime I start VSCode I have a message saying my elan is too old and proposing to update. I always accept but it never updates.

[Sebastian Ullrich]

Which elan version? 3.1.0 has a bug where the update does nothing, so elan has to be reinstalled manually.

[Marc Huisinga]

Patrick Massot said:

I think something is not working. Marc Huisinga everytime I start VSCode I have a message saying my elan is too old and proposing to update. I always accept but it never updates.

It should display an error with a "Show Output" button that takes you to the elan self update output. What does it say there?

Sebastian Ullrich said:

Which elan version? 3.1.0 has a bug where the update does nothing, so elan has to be reinstalled manually.

Oh, that's really bad. I might need to add additional special handling for 3.1.0 then.

[Marc Huisinga]

Ah, I know why it doesn't display an error and Patrick is confused. Elan doesn't even return an error exit code when this bug occurs on 3.1.0 :/

[Patrick Massot]

Yes, I have 3.1.0

[Marc Huisinga]

Patrick Massot said:

I think something is not working. Marc Huisinga everytime I start VSCode I have a message saying my elan is too old and proposing to update. I always accept but it never updates.

This should be fixed in the recent pre-release. VS Code will now instead re-run the installation script for Elan 3.1.0 specifically, which also updates Elan.

[Patrick Massot]

I can confirm VSCode succeeded to update my elan. Thanks!

[Marc Huisinga]

This has been released to everyone now. If you encounter any new issues, please let me know.