feat: better setup diagnostics

[mhuisi]

This PR has three main goals:

1. Implement a new and easily extensible mechanism to detect issues with the user's setup and notify them about it.
2. Implement an easily extensible mechanism to dump all kinds of context information about the user's system and Lean setup to make it easier to debug issues with their setup.
3. Clean up all of the existing code to the extent that is necessary in order to facilitate 1. and 2..

Setup diagnostic warnings and errors

There are two separate kinds of setup diagnostics: Global- and project-level diagnostics.

• Global-level diagnostics are checked when the first Lean file is opened. If there is an error-level setup issue, none of the Lean-specific extension features are activated. The following global-level aspects of the user's setup are checked:
  1. Whether Curl and Git are installed (Error; reference to setup guide)
  2. Whether some version of Lean can be found (Error; Elan installation offered)
  3. Whether Elan is installed and reasonably up-to-date (Warning; Elan installation / Elan update offered)
• Project-level diagnostics are checked whenever the first Lean file of a project is opened. If there is an error-level setup issue, the language client will not launch, but all of the other Lean-specific extension features will be active, provided that the global-level diagnostics did not yield an error. The following project-level aspects of the user's setup are checked:
  1. Whether the language client is running in an Untitled file without an attached Lean 4 project (Warning; reference to setup guide)
  2. Whether a lean-toolchain file can be found in the project associated with the file (Warning; reference to setup guide & option to open parent directory with lean-toolchain offered if present)
  3. Whether some version of Lean can be found (Error)
  4. Whether the project associated with the file is a Lean 3 project (Error)
  5. Whether the project associated with the file is using a Lean version from before the first Lean 4 stable release (Warning)
  6. Whether some version of Lake can be found (Error)

If someone is willingly using a "weird" setup that triggers warning-level diagnostics, the corresponding notifications can be turned off using the lean4.showSetupWarnings configuration option.

Setup diagnostic dump

In the forall menu, a new command "Troubleshooting: Show Setup Information" has been added that can be used to gather information about the user's system and their Lean setup. It includes the following information:

1. Operating system
2. CPU architecture
3. CPU model
4. Total available RAM
5. Whether Curl is installed
6. Whether Git is installed
7. Whether Elan is installed and reasonably up-to-date, as well as the Elan version
8. Whether Lean is installed and reasonably up-to-date, as well as the Lean version
9. Whether a Lean project with a lean-toolchain has been opened, as well as the path to the project
10. Available Elan toolchains

Clean-up of user-facing legacy features

• Several settings to modify the commands that are launched in specific situations have been removed (lean4.toolchainPath, lean4.lakePath, lean4.enableLake, lean4.serverEnv, lean4.serverEnvPaths) and replaced with a single setting lean4.envPathExtensions that can be used to augment the PATH variable of the VS Code extension process and all of its child processes.
• Compatibility with Lean versions that did not support lake serve has been removed.
• The exports of the extension have been cleaned up to reflect the two-stage activation of the extension (first, non-Lean specific features are activated when VS Code is launched, second, Lean-specific features are activated when a Lean file is opened).
• When opening a project and installing Elan for the first time, the extension would install the given project toolchain as the default Elan toolchain and then use that toolchain for the project as well. This saves some bandwidth and is a bit quicker, but comes at the disadvantage that users will have a project-specific toolchain installed as their global default toolchain, potentially leading to unintuitive behavior down the road (e.g. when creating new projects). Now, we instead install two toolchains in this scenario: leanprover/lean4:stable as the default toolchain, and the project-specific toolchain for that project. In the future, when Eagerly resolve toolchains to canonical, fixed reference elan#106 lands, this should lead to much more intuitive behavior outside of projects.

Refactorings

• Much of the old bootstrapping and Lean version check logic has been rewritten and entirely replaced with the new setup diagnostic system. Most importantly, the Lean installation bootstrapping deep in LeanClientProvider has been lifted out to the outer global-level setup diagnostics and the LeanClientProvider is now much simpler than it used to be.
• The version cache in LeanClientProvider has been deleted. Calling lean --version (rarely) a second time when that specific Lean toolchain has already been installed by a previous call should be sufficiently cheap that no cache should be needed.
• config.ts has been cleaned up.
• The tests for setups without Elan have been removed as they only worked due to special test-specific behavior in the first place. I'd like to re-add better tests for this at some point in the future.
• The pre-bootstrap test has been removed because it did not properly test whether the installation prompt is open. It would be nice to have proper tests for all setup diagnostics eventually, anyways.
• The Typescript version has been updated 5.4.5.
• Progress bars are now only displayed after 250ms to reduce visual clutter for quick-running commands.
• All calls to window.show(Error|Warning|Information)... have been refactored to use a safer API that ensures the following invariants to prevent the VS Code extension from being blocked on a transient notification:
  • Notifications without input should never block the extension
  • Notifications with optional input should never block the extension
  • Notifications that block the extension must be modal

Affected issues

Fixes #323: We now have a general mechanism to improve these kinds of setup issues.
Closes #326: This setting has been removed.
Fixes #388: The refactored startup logic respects overrides.
Closes #400: This setting has been removed.
Closes #440: This setting has been removed. I checked with @eric-wieser to make sure that the setup exhibiting this issue can be implemented without this setting as well.