Add project commands, command menu and walkthrough

[mhuisi]

This PR adds several new commands, a command menu UI, a walkthrough guide that is displayed when the extension is installed and several related usability improvements. It also adds CI support for pre-releases.

New commands

Creating Projects

Two new commands to create projects have been added: lean4.project.createStandaloneProject and lean4.project.createMathlibProject.

Both commands display a file picker to select the location to create the project at, update Elan before creating the project, create the project using lake init and then run lake update to generate the lake-manifest.json file. Standalone projects use leanprover/lean4:stable for their toolchain; mathlib projects use leanprover-community/mathlib4:lean-toolchain.

After creating a mathlib project, lake exe cache get is called.

When the project is fully initialized, users are prompted whether they want to open the newly created project.

Opening Projects

Two new commands to open existing projects have been added: lean4.project.open and lean4.project.clone.

lean4.project.open is intended to prevent users from accidentally opening the wrong folder. It displays a file picker and then checks if the selected folder is a valid Lean 4 project. The heuristic used here is the same as the one that has been used in the extension so far: If it contains a lean-toolchain file it is a valid Lean 4 project. If it contains LICENSE and LICENSES files, as well as a src folder, it is assumed to be Lean 4 itself and can also be opened with the command.
If the selected folder is not a valid Lean 4 project, the command looks through parent folders to see if it can find one there. If it finds one, it suggests to open that one instead.

lean4.project.clone shows an input that allows users to input a URL to a Git repository. Afterwards, a file picker is opened to select the folder to clone the project to. Then, it clones the project using git clone, attempts to fetch the mathlib cache using lake exe cache get (failing silently if the command is not available) and asks whether the new project should be opened.

Lake Commands

Four new commands for common Lake operations have been added: lean4.project.build, lean4.project.clean, lean4.project.updateDependency and lean4.project.fetchCache. All of these commands can interfere with the language server, so the Lean client is automatically stopped before running the command and automatically restarted afterwards.

lean4.project.build fetches the mathlib cache if it is available and runs lake build afterwards.

lean4.project.clean displays a confirmation prompt, runs lake clean and then asks the user whether they want to immediately fetch the mathlib cache if lake exe cache is available.

lean4.project.fetchCache simply fetches the mathlib cache if lake exe cache is available.

lean4.updateDependency parses the manifest.json of the project that is currently selected and fetches the current remote revision for each by calling git ls-remote with the input revision designated in the manifest. Dependencies that are still up-to-date are filtered. Then, a selection dialog is displayed to choose the dependency to update, what revision it is currently on and which one it will be updated to.
After selecting a dependency, if the project is a GitHub project, the current remote lean-toolchain is automatically determined. If it differs from the current lean-toolchain of the project, a prompt is displayed, asking the user if they want to update their lean-toolchain to the remote version. If the project is not a GitHub project, users are asked whether they want to continue with updating the dependency without also updating the toolchain version.
Finally, the new toolchain version is written, lake update is called to update the selected dependency and the mathlib cache is fetched if lake exe cache is available.

Elan

The command to install elan that used to be only accessible by opening a new Lean 4 file without having Lean installed has also been exposed as a command lean4.setup.installElan now.

Command Menu

In the top right, a new menu with the ∀-quantifier from Lean's logo as an icon has been added. The menu provides access to all user-facing commands that the VS Code extension provides.

Since the menu can be used to open and create projects, as well as access documentation related to Lean, it is always displayed, even if no Lean 4 project is open. If one finds this annoying, it can be disabled with a new configuration setting. Certain commands are however only displayed when a Lean 4 file is open, e.g. building the project, as we need a file to determine the project that is currently active in multi-root workspaces.

Walkthrough

When the extension is first installed, a platform-specific walkthrough guide is opened that provides information on the following:

• Learning Lean: Links to books, the natural number game and documentation, as well as which target group each resource is intended for.
• Installing dependencies: A short platform-specific guide to get users set-up with Git and curl.
• Installing Elan: A button to install Elan from the walkthrough.
• Projects: A list of buttons that can be pressed to create a new project or obtain an existing one using the aforementioned commands.
• Zulip: An invitation to the Lean Zulip, a short introduction on how to post there and how to post helpful code examples.

The walkthrough can always be re-opened through the "Documentation" submenu in the command menu.

Safeguards

If users accidentally open a folder that is not a Lean 4 project using VS Code's regular "Open Folder" command and then open a Lean file within it, a notification suggesting that a wrong folder has been opened is displayed. If there is a parent folder that is a valid Lean 4 project, the notification suggests to open that folder instead.

If users open a single Lean 4 file, a notification is displayed informing them that not all features are available in this mode and that they should open a project instead.

Both notifications can be disabled with a new configuration setting.

Other Usability Improvements

1. When selecting to restart the server, a confirmation prompt is displayed beforehand.
2. A progress bar is displayed while starting the language server.
3. All expensive external commands now display a progress bar.
4. The progress bar notification now always contains a link to open the output channel where all command output is dumped for troubleshooting purposes.
5. When errors are displayed for any external commands, a button is now displayed to open the command output.
6. All external commands for which a progress bar is displayed can be cancelled by pressing the "Cancel" button on the progress notification. Doing so will terminate the command process.
7. The output channel now also displays the external commands that have been invoked, not just their output.
8. The "Restart File" command can now be activated using the context menu by right clicking in a file.
9. The extension does not ask to install Lean on markdown files anymore.

[mhuisi]

The tests are currently broken due to the fact that the extension activation logic changed, which means that some components of the extension are exported later after activation than they used to, and so the tests can't find them. I will resolve this later; I want to get these changes out for a pre-release ASAP.

[mhuisi]

Please still feel free to review this PR, as it will not be fully released until 2023-10-22.