diff --git a/.github/workflows/on-push.yml b/.github/workflows/on-push.yml index feab98fe4..975998d5f 100644 --- a/.github/workflows/on-push.yml +++ b/.github/workflows/on-push.yml @@ -43,7 +43,14 @@ jobs: npm ci npx lerna bootstrap --ci npm run build - npx lerna run --scope=lean4 package + + - name: Package + run: npx lerna run --scope=lean4 package + if: ${{ !startsWith(github.ref, 'refs/tags/v') || !endsWith(github.ref, '-pre') }} + + - name: Package pre-release + run: npx lerna run --scope=lean4 packagePreRelease + if: ${{ startsWith(github.ref, 'refs/tags/v') && endsWith(github.ref, '-pre') }} - name: Upload artifact uses: actions/upload-artifact@v2 @@ -53,7 +60,7 @@ jobs: path: 'vscode-lean4/lean4-*.vsix' - name: Publish packaged extension - if: startsWith(github.ref, 'refs/tags/v') && matrix.os == 'ubuntu-latest' + if: ${{ startsWith(github.ref, 'refs/tags/v') && !endsWith(github.ref, '-pre') && matrix.os == 'ubuntu-latest' }} run: | cd vscode-lean4 npx vsce publish -i lean4-*.vsix @@ -62,6 +69,16 @@ jobs: OVSX_PAT: ${{ secrets.OVSX_PAT }} VSCE_PAT: ${{ secrets.VSCE_PAT }} + - name: Publish packaged pre-release extension + if: ${{ startsWith(github.ref, 'refs/tags/v') && endsWith(github.ref, '-pre') && matrix.os == 'ubuntu-latest' }} + run: | + cd vscode-lean4 + npx vsce publish --pre-release -i lean4-*.vsix + npx ovsx publish --pre-release lean4-*.vsix + env: + OVSX_PAT: ${{ secrets.OVSX_PAT }} + VSCE_PAT: ${{ secrets.VSCE_PAT }} + - name: Upload extension as release if: startsWith(github.ref, 'refs/tags/v') && matrix.os == 'ubuntu-latest' uses: softprops/action-gh-release@v1 diff --git a/.vscode/settings.json b/.vscode/settings.json index 512315c94..5e457541a 100644 --- a/.vscode/settings.json +++ b/.vscode/settings.json @@ -8,5 +8,8 @@ }, "typescript.tsdk": "./node_modules/typescript/lib", // we want to use the TS server from our node_modules folder to control its version "files.insertFinalNewline": true, - "files.trimTrailingWhitespace": true + "files.trimTrailingWhitespace": true, + "[markdown]": { + "files.trimTrailingWhitespace": false + } } diff --git a/prerelease.sh b/prerelease.sh new file mode 100755 index 000000000..38e994444 --- /dev/null +++ b/prerelease.sh @@ -0,0 +1,13 @@ +#!/bin/sh +if [ $# != 1 ]; then + echo Usage: ./prerelease.sh 1.2.3 + exit 1 +fi + +new_version="$1" +sed -i 's/"version": ".*"/"version": "'$new_version'"/' vscode-lean4/package.json +git commit -am "Release $new_version (pre-release)" +git tag -a v$new_version-pre -m "vscode-lean4 $new_version (pre-release)" + +git push +git push --tags diff --git a/vscode-lean4/media/guide-documentation.md b/vscode-lean4/media/guide-documentation.md new file mode 100644 index 000000000..690c16cc6 --- /dev/null +++ b/vscode-lean4/media/guide-documentation.md @@ -0,0 +1,26 @@ +## Books +If you want to learn Lean 4, choose one of the following introductory books based on your background. If you are getting stuck or have any questions, click on the 'Questions and Troubleshooting' step at the bottom on the left side. + +- [Functional Programming in Lean](https://lean-lang.org/functional_programming_in_lean/) + The standard introduction for using Lean 4 as a general-purpose programming language. +- [The Mechanics of Proof](https://hrmacbeth.github.io/math2001/) + An introduction to Lean 4 as an interactive theorem prover for anyone who also wants to learn how to write rigorous mathematical proofs. +- [Mathematics in Lean](https://leanprover-community.github.io/mathematics_in_lean/) + The standard introduction to Lean 4 as an interactive theorem prover for users with a mathematics background. +- [Theorem Proving in Lean 4](https://lean-lang.org/theorem_proving_in_lean4/) + The standard reference for using Lean 4 as an interactive theorem prover. Suited as an introduction for users with a computer science background, advanced users and for general use as a reference manual. + +Once you have completed one of these books and its exercises, you are ready to use Lean 4 for your own projects. If you want to use Lean 4 both as a general-purpose programming language and an interactive theorem prover, it is recommended to read both [Functional Programming in Lean](https://lean-lang.org/functional_programming_in_lean/) and [Theorem Proving in Lean 4](https://lean-lang.org/theorem_proving_in_lean4/). + +## Hands-On Tutorial +If you want to dive right into using Lean 4 to prove elementary theorems about natural numbers, you can play the [Natural Number Game](https://adam.math.hhu.de/#/g/hhu-adam/NNG4). It can be played online using your browser without a local installation. + +## Additional Resources +**Website** +[Lean's website](https://lean-lang.org/) links to learning resources, publications, talks and articles about Lean. + +**Lean Community** +The [Lean Community website](https://leanprover-community.github.io/index.html) links to several other helpful learning resources not listed here and provides an introduction to [mathlib](https://github.com/leanprover-community/mathlib4), Lean's math library. + +**Manual** +The [Lean Manual](https://lean-lang.org/lean4/doc/) documents several features of Lean 4 and can be consulted for some of the more technical details concerning Lean. diff --git a/vscode-lean4/media/guide-help.md b/vscode-lean4/media/guide-help.md new file mode 100644 index 000000000..39212f0e8 --- /dev/null +++ b/vscode-lean4/media/guide-help.md @@ -0,0 +1,8 @@ +## Asking Questions on the Lean Zulip Chat + +To post your question on the [Lean Zulip chat](https://leanprover.zulipchat.com/), you can follow these steps: +1. [Create a new Lean Zulip chat account](https://leanprover.zulipchat.com/register/). +2. [Visit the #new-members stream](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members). +3. Click the 'New topic' button at the bottom of the page, enter a topic title, describe your question or issue in the message text box and click 'Send'. + +When posting code on the Lean Zulip chat, please reduce the code to a [minimal working example](https://leanprover-community.github.io/mwe.html) that includes all imports and declarations needed for others to copy and paste the code into their own development environment. Please also make sure to delimit the code by [three backticks](https://github.com/leanprover-community/mathlib/wiki/Code-in-backticks) so that the code is highlighted and formatted correctly. diff --git a/vscode-lean4/media/guide-installDeps-linux.md b/vscode-lean4/media/guide-installDeps-linux.md new file mode 100644 index 000000000..8ece155d0 --- /dev/null +++ b/vscode-lean4/media/guide-installDeps-linux.md @@ -0,0 +1,18 @@ +## Installing Required Dependencies +1. [Open a new terminal](command:workbench.action.terminal.new). +2. Depending on your Linux distribution, do one of the following to install Git and curl using your package manager: + * On Ubuntu and Debian, type in `sudo apt install git curl` and press Enter. + * On Fedora, type in `sudo dnf install git curl` and press Enter. + * If you are not sure which Linux distribution you are using, you can try both. +3. When prompted, type in your login credentials. +4. Wait until the installation has completed. + +## Dependencies Needed by Lean 4 +[Git](https://git-scm.com/) is a commonly used [Version Control System](https://en.wikipedia.org/wiki/Version_control) that is used by Lean to help manage different versions of Lean formalization packages and software packages. + +[curl](https://curl.se/) is a small tool to transfer data that is used by Lean to download files when managing Lean formalization packages and software packages. + +## Restricted Environments +If you are in an environment where you cannot install Git or curl, for example a restricted university computer, you can check if you already have them installed by [opening a new terminal](command:workbench.action.terminal.new), typing in `which git curl` and pressing Enter. If the terminal output displays two file paths and no error, you already have them installed. + +If your machine does not already have Git and curl installed and you cannot install them, there is currently no option to try Lean 4 with a local installation. If you want to try out Lean 4 regardless, you can read [Mathematics in Lean](https://leanprover-community.github.io/mathematics_in_lean/) and do the exercises with [an online instance of Lean 4 hosted using Gitpod](https://gitpod.io/#/https://github.com/leanprover-community/mathematics_in_lean). Doing so requires creating a GitHub account. diff --git a/vscode-lean4/media/guide-installDeps-mac.md b/vscode-lean4/media/guide-installDeps-mac.md new file mode 100644 index 000000000..9617e2a24 --- /dev/null +++ b/vscode-lean4/media/guide-installDeps-mac.md @@ -0,0 +1,16 @@ +## Installing Required Dependencies +1. [Open a new terminal](command:workbench.action.terminal.new). +2. Type in `/bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/HEAD/install.sh)"` and press Enter to install [Homebrew](https://brew.sh/), a package manager for macOS. +3. Follow the instructions in the terminal. +4. Type in `brew install curl git` and press Enter. +5. Wait until the installation has completed. + +## Dependencies Needed by Lean 4 +[Git](https://git-scm.com/) is a commonly used [Version Control System](https://en.wikipedia.org/wiki/Version_control) that is used by Lean to help manage different versions of Lean formalization packages and software packages. + +[curl](https://curl.se/) is a small tool to transfer data that is used by Lean to download files when managing Lean formalization packages and software packages. + +## Restricted Environments +If you are in an environment where you cannot install Homebrew, Git or curl, for example a restricted university computer, you can check if you already have them installed by [opening a new terminal](command:workbench.action.terminal.new), typing in `which git curl` and pressing Enter. If the terminal output displays two file paths and no error, you already have them installed. + +If your machine does not already have Homebrew, Git and curl installed and you cannot install them, there is currently no option to try Lean 4 with a local installation. If you want to try out Lean 4 regardless, you can read [Mathematics in Lean](https://leanprover-community.github.io/mathematics_in_lean/) and do the exercises with [an online instance of Lean 4 hosted using Gitpod](https://gitpod.io/#/https://github.com/leanprover-community/mathematics_in_lean). Doing so requires creating a GitHub account. diff --git a/vscode-lean4/media/guide-installDeps-windows.md b/vscode-lean4/media/guide-installDeps-windows.md new file mode 100644 index 000000000..324bead4f --- /dev/null +++ b/vscode-lean4/media/guide-installDeps-windows.md @@ -0,0 +1,9 @@ +## Installing Required Dependencies +1. Install [Git](https://git-scm.com/download/win). You can keep all settings in the installer at their default values. +2. Wait until the installation has completed. +3. Restart VS Code and re-open this guide. + +[Git](https://git-scm.com/) is a commonly used [Version Control System](https://en.wikipedia.org/wiki/Version_control) that is used by Lean to help manage different versions of Lean formalization packages and software packages. + +## Restricted Environments +If you are in an environment where you cannot install Git and it is not already installed, for example on a restricted university computer, there is currently no option to try Lean 4 with a local installation. If you want to try out Lean 4 regardless, you can read [Mathematics in Lean](https://leanprover-community.github.io/mathematics_in_lean/) and do the exercises with [an online instance of Lean 4 hosted using Gitpod](https://gitpod.io/#/https://github.com/leanprover-community/mathematics_in_lean). Doing so requires creating a GitHub account. diff --git a/vscode-lean4/media/guide-installElan-unix.md b/vscode-lean4/media/guide-installElan-unix.md new file mode 100644 index 000000000..1acdaceac --- /dev/null +++ b/vscode-lean4/media/guide-installElan-unix.md @@ -0,0 +1,4 @@ +## Elan +[Elan](https://github.com/leanprover/elan) automatically manages all the different versions of Lean and ensures that the correct version is used when opening a project. + +Clicking [this link](command:lean4.setup.installElan) will download the [Elan setup script](https://github.com/leanprover/elan/blob/master/elan-init.sh) and execute it. diff --git a/vscode-lean4/media/guide-installElan-windows.md b/vscode-lean4/media/guide-installElan-windows.md new file mode 100644 index 000000000..c56099c17 --- /dev/null +++ b/vscode-lean4/media/guide-installElan-windows.md @@ -0,0 +1,4 @@ +## Elan +[Elan](https://github.com/leanprover/elan) automatically manages all the different versions of Lean and ensures that the correct version is used when opening a project. + +Clicking [this link](command:lean4.setup.installElan) will download the [Elan setup script](https://github.com/leanprover/elan/blob/master/elan-init.ps1) and execute it. diff --git a/vscode-lean4/media/guide-setupProject.md b/vscode-lean4/media/guide-setupProject.md new file mode 100644 index 000000000..53648a304 --- /dev/null +++ b/vscode-lean4/media/guide-setupProject.md @@ -0,0 +1,15 @@ +## Project Creation +If you want to create a new project, click on one of the following: +- [Create a new standalone project](command:lean4.project.createStandaloneProject) + Standalone projects do not depend on any other Lean 4 projects. Dependencies can be added by modifying 'lakefile.lean' in the newly created project as described [here](https://github.com/leanprover/lean4/blob/master/src/lake/README.md#adding-dependencies). +- [Create a new mathlib project](command:lean4.project.createMathlibProject) + Mathlib projects depend on [mathlib](https://github.com/leanprover-community/mathlib4), the math library of Lean 4. + +If you want to open an existing project, click on one of the following: +- [Download an existing project](command:lean4.project.clone) +- [Open an existing local project](command:lean4.project.open) + +After creating or downloading a project, you can open it in the future by clicking the ∀-symbol in the top right, choosing 'Open Project…' > 'Open Local Project…' and selecting the project you created. + +## Complex Project Setups +Using its build system and package manager Lake, Lean 4 supports more complex project setups than the ones described above. You can find out more about Lake in the [Lean 4 GitHub repository](https://github.com/leanprover/lean4/blob/master/src/lake/README.md). diff --git a/vscode-lean4/media/lean-mini-dark.svg b/vscode-lean4/media/lean-mini-dark.svg new file mode 100644 index 000000000..5ba4d929f --- /dev/null +++ b/vscode-lean4/media/lean-mini-dark.svg @@ -0,0 +1,259 @@ + + + + + + image/svg+xml + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/vscode-lean4/media/lean-mini-light.svg b/vscode-lean4/media/lean-mini-light.svg new file mode 100644 index 000000000..691cdc68c --- /dev/null +++ b/vscode-lean4/media/lean-mini-light.svg @@ -0,0 +1,259 @@ + + + + + + image/svg+xml + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/vscode-lean4/media/open-setup-guide.png b/vscode-lean4/media/open-setup-guide.png new file mode 100644 index 000000000..c86e98464 Binary files /dev/null and b/vscode-lean4/media/open-setup-guide.png differ diff --git a/vscode-lean4/package-lock.json b/vscode-lean4/package-lock.json index a0305afbe..66132b397 100644 --- a/vscode-lean4/package-lock.json +++ b/vscode-lean4/package-lock.json @@ -1,19 +1,20 @@ { "name": "lean4", - "version": "0.0.111", + "version": "0.0.113", "lockfileVersion": 3, "requires": true, "packages": { "": { "name": "lean4", - "version": "0.0.111", + "version": "0.0.113", "license": "Apache-2.0", "dependencies": { "axios": "~0.24.0", "cheerio": "^1.0.0-rc.10", "mobx": "5.15.7", "semver": "=7.3.5", - "vscode-languageclient": "=8.0.2" + "vscode-languageclient": "=8.0.2", + "zod": "^3.22.4" }, "devDependencies": { "@types/cheerio": "~0.22.30", @@ -37,7 +38,7 @@ "webpack-cli": "^4.10.0" }, "engines": { - "vscode": "^1.70.0" + "vscode": "^1.75.0" } }, "node_modules/@babel/runtime": { @@ -4661,6 +4662,14 @@ "funding": { "url": "https://github.com/sponsors/sindresorhus" } + }, + "node_modules/zod": { + "version": "3.22.4", + "resolved": "https://registry.npmjs.org/zod/-/zod-3.22.4.tgz", + "integrity": "sha512-iC+8Io04lddc+mVqQ9AZ7OQ2MrUKGN+oIQyq1vemgt46jwCwLfhq7/pwnBnNXXXZb8VTVLKwp9EDkx+ryxIWmg==", + "funding": { + "url": "https://github.com/sponsors/colinhacks" + } } } } diff --git a/vscode-lean4/package.json b/vscode-lean4/package.json index 81bc86f30..411f62449 100644 --- a/vscode-lean4/package.json +++ b/vscode-lean4/package.json @@ -5,7 +5,7 @@ "version": "0.0.113", "publisher": "leanprover", "engines": { - "vscode": "^1.70.0" + "vscode": "^1.75.0" }, "categories": [ "Programming Languages" @@ -25,7 +25,7 @@ "lean4.toolchainPath": { "type": "string", "default": "", - "markdownDescription": "Path to your Lean toolchain. Leave this blank to get the default location from your PATH environment or from the default elan install location.", + "markdownDescription": "**DO NOT CHANGE** unless you know what you are doing. Path to your Lean toolchain. Leave this blank to get the default location from your PATH environment or from the default elan install location.", "scope": "machine-overridable" }, "lean4.input.enabled": { @@ -179,6 +179,16 @@ "type": "number", "default": 200, "description": "Time (in milliseconds) which must pass since latest edit until elaboration begins. Lower values may make editing feel faster at the cost of higher CPU usage." + }, + "lean4.showInvalidProjectWarnings": { + "type": "boolean", + "default": true, + "markdownDescription": "Show warnings whenever a .lean-file is opened in a folder that does not contain a 'lean-toolchain' file." + }, + "lean4.alwaysShowTitleBarMenu": { + "type": "boolean", + "default": true, + "markdownDescription": "Always display the Lean extension title bar menu in the top right. This helps beginners create and open Lean projects after launching an empty instance of VS Code, but may not be desirable for anyone who uses VS Code for things other than Lean." } } }, @@ -186,25 +196,25 @@ { "command": "lean4.restartServer", "category": "Lean 4", - "title": "Restart Server", + "title": "Server: Restart Server", "description": "Restart the Lean server (for all files)." }, { "command": "lean4.stopServer", "category": "Lean 4", - "title": "Stop Server", + "title": "Server: Stop Server", "description": "Stop the Lean server (for all files)." }, { "command": "lean4.restartFile", "category": "Lean 4", - "title": "Restart File", + "title": "Server: Restart File", "description": "Restarts the Lean server for the file that is currently focused, refreshing the dependencies." }, { "command": "lean4.refreshFileDependencies", "category": "Lean 4", - "title": "Refresh File Dependencies", + "title": "Server: Refresh File Dependencies", "description": "Restarts the Lean server for the file that is currently focused to refresh the dependencies." }, { @@ -226,7 +236,7 @@ { "command": "lean4.toggleInfoview", "category": "Lean 4", - "title": "Infoview: Toggle", + "title": "Infoview: Toggle Infoview", "description": "Toggle whether the infoview is displayed." }, { @@ -266,14 +276,92 @@ { "command": "lean4.docView.showAllAbbreviations", "category": "Lean 4", - "title": "Show all abbreviations", + "title": "Docview: Show All Abbreviations", "description": "Show help page containing all abbreviations and the Unicode characters they map to." }, { "command": "lean4.docView.open", "category": "Lean 4", - "title": "Open Documentation View", + "title": "Docview: Open Docview", "description": "Open documentation found in local 'html' folder in a separate web view panel." + }, + { + "command": "lean4.docView.back", + "category": "Lean 4", + "title": "Docview: Back", + "description": "Go to previous page in documentation view" + }, + { + "command": "lean4.docView.forward", + "category": "Lean 4", + "title": "Docview: Forward", + "description": "Go to next page in documentation view" + }, + { + "command": "lean4.troubleshooting.showOutput", + "category": "Lean 4", + "title": "Troubleshooting: Show Output", + "description": "Show output channel containing all progress updates and errors of commands" + }, + { + "command": "lean4.setup.showSetupGuide", + "category": "Lean 4", + "title": "Setup: Show Setup Guide", + "description": "Show 'Welcome' page containing a checklist of steps to install Lean 4" + }, + { + "command": "lean4.setup.installElan", + "category": "Lean 4", + "title": "Setup: Install Elan", + "description": "Install Lean's version manager 'Elan'" + }, + { + "command": "lean4.project.createStandaloneProject", + "category": "Lean 4", + "title": "Project: Create Standalone Project…", + "description": "Create a new Lean project that does not depend on any other projects" + }, + { + "command": "lean4.project.createMathlibProject", + "category": "Lean 4", + "title": "Project: Create Mathlib Project…", + "description": "Create a new Lean math formalization project using Mathlib" + }, + { + "command": "lean4.project.open", + "category": "Lean 4", + "title": "Project: Open Local Project…", + "description": "Opens a local Lean project" + }, + { + "command": "lean4.project.clone", + "category": "Lean 4", + "title": "Project: Download Project…", + "description": "Download an existing Lean project using `git clone`" + }, + { + "command": "lean4.project.build", + "category": "Lean 4", + "title": "Project: Build Project", + "description": "Build the current project" + }, + { + "command": "lean4.project.clean", + "category": "Lean 4", + "title": "Project: Clean Project", + "description": "Clean the current project, removing all build artifacts" + }, + { + "command": "lean4.project.updateDependency", + "category": "Lean 4", + "title": "Project: Update Dependency…", + "description": "Updates a dependency of the current project to the most recent version available for the branch pinned in 'lakefile.lean'." + }, + { + "command": "lean4.project.fetchCache", + "category": "Lean 4", + "title": "Project: Fetch Mathlib Build Cache", + "description": "Downloads cached Mathlib build artifacts to avoid full elaboration" } ], "languages": [ @@ -351,17 +439,37 @@ "menus": { "commandPalette": [ { - "command": "lean4.input.convert", - "when": "editorLangId == lean4 && lean4.input.isActive" + "command": "lean4.restartServer", + "when": "editorLangId == lean4" + }, + { + "command": "lean4.stopServer", + "when": "editorLangId == lean4" }, { "command": "lean4.restartFile", "when": "editorLangId == lean4" }, + { + "command": "lean4.refreshFileDependencies", + "when": "editorLangId == lean4" + }, + { + "command": "lean4.input.convert", + "when": "editorLangId == lean4 && lean4.input.isActive" + }, { "command": "lean4.displayGoal", "when": "editorLangId == lean4" }, + { + "command": "lean4.toggleInfoview", + "when": "editorLangId == lean4" + }, + { + "command": "lean4.displayList", + "when": "editorLangId == lean4" + }, { "command": "lean4.infoView.copyToComment", "when": "editorLangId == lean4" @@ -371,34 +479,226 @@ "when": "editorLangId == lean4" }, { - "command": "lean4.restartServer", + "command": "lean4.infoView.toggleUpdating", "when": "editorLangId == lean4" }, { - "command": "lean4.stopServer", + "command": "lean4.infoView.toggleExpectedType", "when": "editorLangId == lean4" }, { - "command": "lean4.restartFile", + "command": "lean4.docView.showAllAbbreviations", "when": "editorLangId == lean4" }, { - "command": "lean4.refreshFileDependencies", + "command": "lean4.docView.open" + }, + { + "command": "lean4.docView.back" + }, + { + "command": "lean4.docView.forward" + }, + { + "command": "lean4.troubleshooting.showOutput" + }, + { + "command": "lean4.setup.showSetupGuide" + }, + { + "command": "lean4.setup.installElan" + }, + { + "command": "lean4.project.createStandaloneProject" + }, + { + "command": "lean4.project.createMathlibProject" + }, + { + "command": "lean4.project.open" + }, + { + "command": "lean4.project.clone" + }, + { + "command": "lean4.project.build", "when": "editorLangId == lean4" }, { - "command": "lean4.docView.showAllAbbreviations", + "command": "lean4.project.clean", + "when": "editorLangId == lean4" + }, + { + "command": "lean4.project.updateDependency", + "when": "editorLangId == lean4" + }, + { + "command": "lean4.project.fetchCache", "when": "editorLangId == lean4" } ], "editor/title": [ { - "command": "lean4.displayGoal", + "submenu": "lean4.titlebar", + "when": "config.lean4.alwaysShowTitleBarMenu || lean4.isLeanFeatureSetActive", + "group": "navigation@0" + } + ], + "lean4.titlebar": [ + { + "submenu": "lean4.titlebar.newProject", + "when": "config.lean4.alwaysShowTitleBarMenu || lean4.isLeanFeatureSetActive", + "group": "1_setup@1" + }, + { + "submenu": "lean4.titlebar.openProject", + "when": "config.lean4.alwaysShowTitleBarMenu || lean4.isLeanFeatureSetActive", + "group": "1_setup@1" + }, + { + "command": "lean4.restartFile", + "when": "lean4.isLeanFeatureSetActive", + "group": "2_server@1" + }, + { + "command": "lean4.restartServer", + "when": "lean4.isLeanFeatureSetActive", + "group": "2_server@2" + }, + { + "command": "lean4.toggleInfoview", + "when": "lean4.isLeanFeatureSetActive", + "group": "3_infoview@1" + }, + { + "command": "lean4.troubleshooting.showOutput", + "when": "config.lean4.alwaysShowTitleBarMenu || lean4.isLeanFeatureSetActive", + "group": "4_troubleshooting" + }, + { + "submenu": "lean4.titlebar.versions", + "when": "config.lean4.alwaysShowTitleBarMenu || lean4.isLeanFeatureSetActive", + "group": "5_versions" + }, + { + "submenu": "lean4.titlebar.projectActions", + "when": "config.lean4.alwaysShowTitleBarMenu || lean4.isLeanFeatureSetActive", + "group": "6_projectActions@1" + }, + { + "submenu": "lean4.titlebar.documentation", + "when": "config.lean4.alwaysShowTitleBarMenu || lean4.isLeanFeatureSetActive", + "group": "7_documentation@1" + } + ], + "lean4.titlebar.newProject": [ + { + "command": "lean4.project.createStandaloneProject", + "when": "config.lean4.alwaysShowTitleBarMenu || lean4.isLeanFeatureSetActive", + "group": "1_newProject@1" + }, + { + "command": "lean4.project.createMathlibProject", + "when": "config.lean4.alwaysShowTitleBarMenu || lean4.isLeanFeatureSetActive", + "group": "1_newProject@2" + } + ], + "lean4.titlebar.openProject": [ + { + "command": "lean4.project.open", + "when": "config.lean4.alwaysShowTitleBarMenu || lean4.isLeanFeatureSetActive", + "group": "1_openProject@1" + }, + { + "command": "lean4.project.clone", + "when": "config.lean4.alwaysShowTitleBarMenu || lean4.isLeanFeatureSetActive", + "group": "1_openProject@2" + } + ], + "lean4.titlebar.versions": [ + { + "command": "lean4.setup.installElan", + "when": "config.lean4.alwaysShowTitleBarMenu || lean4.isLeanFeatureSetActive", + "group": "1_setup@1" + } + ], + "lean4.titlebar.projectActions": [ + { + "command": "lean4.project.build", + "when": "lean4.isLeanFeatureSetActive", + "group": "1_projectActions@1" + }, + { + "command": "lean4.project.clean", + "when": "lean4.isLeanFeatureSetActive", + "group": "1_projectActions@2" + }, + { + "command": "lean4.project.updateDependency", + "when": "lean4.isLeanFeatureSetActive", + "group": "1_projectActions@3" + }, + { + "command": "lean4.project.fetchCache", + "when": "lean4.isLeanFeatureSetActive", + "group": "2_mathlibActions@1" + } + ], + "lean4.titlebar.documentation": [ + { + "command": "lean4.setup.showSetupGuide", + "when": "config.lean4.alwaysShowTitleBarMenu || lean4.isLeanFeatureSetActive", + "group": "1_installation@1" + }, + { + "command": "lean4.docView.open", + "when": "config.lean4.alwaysShowTitleBarMenu || lean4.isLeanFeatureSetActive", + "group": "2_docview@1" + }, + { + "command": "lean4.docView.showAllAbbreviations", + "when": "config.lean4.alwaysShowTitleBarMenu || lean4.isLeanFeatureSetActive", + "group": "2_docview@2" + } + ], + "editor/context": [ + { + "command": "lean4.restartFile", "when": "editorLangId == lean4", - "group": "navigation@2" + "group": "z_commands" } ] }, + "submenus": [ + { + "id": "lean4.titlebar", + "label": "Lean 4", + "icon": { + "dark": "./media/lean-mini-dark.svg", + "light": "./media/lean-mini-light.svg" + } + }, + { + "id": "lean4.titlebar.newProject", + "label": "New Project…" + }, + { + "id": "lean4.titlebar.openProject", + "label": "Open Project…" + }, + { + "id": "lean4.titlebar.versions", + "label": "Version Management…" + }, + { + "id": "lean4.titlebar.projectActions", + "label": "Project Actions…" + }, + { + "id": "lean4.titlebar.documentation", + "label": "Documentation…" + } + ], "semanticTokenScopes": [ { "scopes": { @@ -414,16 +714,158 @@ "editor.tabSize": 2, "editor.wordSeparators": "`~@$%^&*()-=+[{]}⟨⟩⦃⦄⟦⟧⟮⟯‹›\\|;:\",.<>/" } - } + }, + "walkthroughs": [ + { + "id": "guide.linux", + "title": "Lean 4 Setup", + "description": "Getting started with Lean 4 on Linux\n", + "when": "isLinux", + "steps": [ + { + "id": "guide.linux.openSetupGuide", + "title": "Re-Open Setup Guide", + "description": "This guide can always be re-opened by opening an empty file, clicking on the ∀-symbol in the top right and selecting 'Documentation…' > 'Setup: Show Setup Guide'.", + "media": { + "image": "media/open-setup-guide.png", + "altText": "Click on the ∀-symbol in the top right and select 'Documentation…' > 'Setup: Show Setup Guide'." + } + }, + { + "id": "guide.linux.documentation", + "title": "Books and Documentation", + "description": "Learn using Lean 4 with the resources on the right.", + "media": { "markdown": "./media/guide-documentation.md" } + }, + { + "id": "guide.linux.installDeps", + "title": "Install Required Dependencies", + "description": "Install Git and curl using your package manager.", + "media": { "markdown": "./media/guide-installDeps-linux.md" } + }, + { + "id": "guide.linux.installElan", + "title": "Install Lean Version Manager", + "description": "Install Lean's version manager Elan.\n[Click to install](command:lean4.setup.installElan)", + "media": { "markdown": "./media/guide-installElan-unix.md" } + }, + { + "id": "guide.linux.setupProject", + "title": "Set Up Lean 4 Project", + "description": "Set up a Lean 4 project by clicking on one of the options on the right.", + "media": { "markdown": "./media/guide-setupProject.md" } + }, + { + "id": "guide.linux.help", + "title": "Questions and Troubleshooting", + "description": "If you have any questions or are having trouble with any of the previous steps, please visit us on the [Lean Zulip chat](https://leanprover.zulipchat.com/) so that we can help you.", + "media": { "markdown": "./media/guide-help.md" } + } + ] + }, + { + "id": "guide.mac", + "title": "Lean 4 Setup", + "description": "Getting started with Lean 4 on Mac\n", + "when": "isMac", + "steps": [ + { + "id": "guide.mac.openSetupGuide", + "title": "Re-Open Setup Guide", + "description": "This guide can always be re-opened by opening an empty file, clicking on the ∀-symbol in the top right and selecting 'Documentation…' > 'Setup: Show Setup Guide'.", + "media": { + "image": "media/open-setup-guide.png", + "altText": "Click on the ∀-symbol in the top right and select 'Documentation…' > 'Setup: Show Setup Guide'." + } + }, + { + "id": "guide.mac.documentation", + "title": "Books and Documentation", + "description": "Learn using Lean 4 with the resources on the right.", + "media": { "markdown": "./media/guide-documentation.md" } + }, + { + "id": "guide.mac.installDeps", + "title": "Install Required Dependencies", + "description": "Install Homebrew, Git and curl.", + "media": { "markdown": "./media/guide-installDeps-mac.md" } + }, + { + "id": "guide.mac.installElan", + "title": "Install Lean Version Manager", + "description": "Install Lean's version manager Elan.\n[Click to install](command:lean4.setup.installElan)", + "media": { "markdown": "./media/guide-installElan-unix.md" } + }, + { + "id": "guide.mac.setupProject", + "title": "Set Up Lean 4 Project", + "description": "Set up a Lean 4 project by clicking on one of the options on the right.", + "media": { "markdown": "./media/guide-setupProject.md" } + }, + { + "id": "guide.mac.help", + "title": "Questions and Troubleshooting", + "description": "If you have any questions or are having trouble with any of the previous steps, please visit us on the [Lean Zulip chat](https://leanprover.zulipchat.com/) so that we can help you.", + "media": { "markdown": "./media/guide-help.md" } + } + ] + }, + { + "id": "guide.windows", + "title": "Lean 4 Setup", + "description": "Getting started with Lean 4 on Windows\n", + "when": "isWindows", + "steps": [ + { + "id": "guide.windows.openSetupGuide", + "title": "Re-Open Setup Guide", + "description": "This guide can always be re-opened by opening an empty file, clicking on the ∀-symbol in the top right and selecting 'Documentation…' > 'Setup: Show Setup Guide'.", + "media": { + "image": "media/open-setup-guide.png", + "altText": "Click on the ∀-symbol in the top right and select 'Documentation…' > 'Setup: Show Setup Guide'." + } + }, + { + "id": "guide.windows.documentation", + "title": "Books and Documentation", + "description": "Learn using Lean 4 with the resources on the right.", + "media": { "markdown": "./media/guide-documentation.md" } + }, + { + "id": "guide.windows.installDeps", + "title": "Install Required Dependencies", + "description": "Install Git.", + "media": { "markdown": "./media/guide-installDeps-windows.md" } + }, + { + "id": "guide.windows.installElan", + "title": "Install Lean Version Manager", + "description": "Install Lean's version manager Elan.\n[Click to install](command:lean4.setup.installElan)", + "media": { "markdown": "./media/guide-installElan-windows.md" } + }, + { + "id": "guide.windows.setupProject", + "title": "Set Up Lean 4 Project", + "description": "Set up a Lean 4 project by clicking on one of the options on the right.", + "media": { "markdown": "./media/guide-setupProject.md" } + }, + { + "id": "guide.windows.help", + "title": "Questions and Troubleshooting", + "description": "If you have any questions or are having trouble with any of the previous steps, please visit us on the [Lean Zulip chat](https://leanprover.zulipchat.com/) so that we can help you.", + "media": { "markdown": "./media/guide-help.md" } + } + ] + } + ] }, "extensionKind": [ "workspace" ], "activationEvents": [ "onLanguage:lean", - "onLanguage:lean4", "onLanguage:markdown", - "onCommand:lean4.restartServer" + "onStartupFinished" ], "main": "./dist/extension", "scripts": { @@ -432,6 +874,7 @@ "watch": "webpack --env development --watch", "watchTest": "concurrently \"tsc -p . -w --outDir out\" \"npm run watch\"", "package": "vsce package", + "packagePreRelease": "vsce package --pre-release", "pretest": "tsc -p . --outDir out", "test": "node ./out/test/suite/runTest.js" }, @@ -442,7 +885,8 @@ "cheerio": "^1.0.0-rc.10", "mobx": "5.15.7", "semver": "=7.3.5", - "vscode-languageclient": "=8.0.2" + "vscode-languageclient": "=8.0.2", + "zod": "^3.22.4" }, "devDependencies": { "@types/cheerio": "~0.22.30", diff --git a/vscode-lean4/src/config.ts b/vscode-lean4/src/config.ts index dd3e498fe..339e327bf 100644 --- a/vscode-lean4/src/config.ts +++ b/vscode-lean4/src/config.ts @@ -223,6 +223,10 @@ export function getElaborationDelay(): number { return workspace.getConfiguration('lean4').get('elaborationDelay', 200); } +export function shouldShowInvalidProjectWarnings(): boolean { + return workspace.getConfiguration('lean4').get('showInvalidProjectWarnings', true) +} + export function getLeanExecutableName(): string { if (process.platform === 'win32') { return 'lean.exe' diff --git a/vscode-lean4/src/docview.ts b/vscode-lean4/src/docview.ts index da133322c..931c9bc3e 100644 --- a/vscode-lean4/src/docview.ts +++ b/vscode-lean4/src/docview.ts @@ -56,11 +56,12 @@ export class DocViewProvider implements Disposable { constructor(extensionUri: Uri) { this.extensionUri = extensionUri; this.subscriptions.push( - commands.registerCommand('lean4.docView.open', (url: string) => this.open(url)), + commands.registerCommand('lean4.docView.open', () => this.open()), + commands.registerCommand('lean4.docView.openUrl', (url: string) => this.open(url)), commands.registerCommand('lean4.docView.back', () => this.back()), commands.registerCommand('lean4.docView.forward', () => this.forward()), - commands.registerCommand('lean4.openTryIt', (code: string) => this.tryIt(code)), - commands.registerCommand('lean4.openExample', (file: string) => this.example(file)), + commands.registerCommand('lean4.docView.openTryIt', (code: string) => this.tryIt(code)), + commands.registerCommand('lean4.docView.openExample', (file: string) => this.example(file)), commands.registerCommand('lean4.docView.showAllAbbreviations', () => this.showAbbreviations()) ); this.subscriptions.push(workspace.onDidCloseTextDocument(doc => { @@ -224,17 +225,17 @@ export class DocViewProvider implements Disposable { } const books : any = { - 'Theorem Proving in Lean': mkCommandUri('lean4.docView.open', 'https://lean-lang.org/theorem_proving_in_lean4/introduction.html'), - 'Functional Programming in Lean': mkCommandUri('lean4.docView.open', 'https://lean-lang.org/functional_programming_in_lean/'), - 'Mathematics in Lean': mkCommandUri('lean4.docView.open', 'https://leanprover-community.github.io/mathematics_in_lean/'), - 'The Mechanics of Proof': mkCommandUri('lean4.docView.open', 'https://hrmacbeth.github.io/math2001/'), - 'Reference Manual': mkCommandUri('lean4.docView.open', 'https://lean-lang.org/lean4/doc/'), + 'Theorem Proving in Lean': mkCommandUri('lean4.docView.openUrl', 'https://lean-lang.org/theorem_proving_in_lean4/introduction.html'), + 'Functional Programming in Lean': mkCommandUri('lean4.docView.openUrl', 'https://lean-lang.org/functional_programming_in_lean/'), + 'Mathematics in Lean': mkCommandUri('lean4.docView.openUrl', 'https://leanprover-community.github.io/mathematics_in_lean/'), + 'The Mechanics of Proof': mkCommandUri('lean4.docView.openUrl', 'https://hrmacbeth.github.io/math2001/'), + 'Reference Manual': mkCommandUri('lean4.docView.openUrl', 'https://lean-lang.org/lean4/doc/'), 'Abbreviations Cheatsheet': mkCommandUri('lean4.docView.showAllAbbreviations'), - 'Example': mkCommandUri('lean4.openExample', 'https://github.com/leanprover/lean4-samples/raw/main/HelloWorld/Main.lean'), + 'Example': mkCommandUri('lean4.docView.openExample', 'https://github.com/leanprover/lean4-samples/raw/main/HelloWorld/Main.lean'), // These are handy for testing that the bad file logic is working. - //'Test bad file': mkCommandUri('lean4.docView.open', Uri.joinPath(this.extensionUri, 'media', 'webview.js')), - //'Test bad Uri': mkCommandUri('lean4.docView.open', 'https://leanprover.github.io/lean4/doc/images/code-success.png'), + //'Test bad file': mkCommandUri('lean4.docView.openUrl', Uri.joinPath(this.extensionUri, 'media', 'webview.js')), + //'Test bad Uri': mkCommandUri('lean4.docView.openUrl', 'https://leanprover.github.io/lean4/doc/images/code-success.png'), }; for (const book of Object.getOwnPropertyNames(books)) { @@ -319,17 +320,17 @@ var side_bar = false; // collapse the side bar menu by default. // here when the html is round tripped through the cheerio parser. } else if (link.attribs.tryitfile) { link.attribs.title = link.attribs.title || 'Open code block (in existing file)'; - link.attribs.href = mkCommandUri('lean4.openExample', new URL(link.attribs.tryitfile as string, url).toString()); + link.attribs.href = mkCommandUri('lean4.docView.openExample', new URL(link.attribs.tryitfile as string, url).toString()); } else if (tryItMatch) { const code = decodeURIComponent(tryItMatch[1] as string); link.attribs.title = link.attribs.title || 'Open code block in new editor'; - link.attribs.href = mkCommandUri('lean4.openTryIt', code); + link.attribs.href = mkCommandUri('lean4.docView.openTryIt', code); } else if (!link.attribs.href.startsWith('command:')) { const hrefUrl = new URL(link.attribs.href as string, url); const isExternal = !url || new URL(url).origin !== hrefUrl.origin; if (!isExternal || hrefUrl.protocol === 'file:') { link.attribs.title = link.attribs.title || link.attribs.href; - link.attribs.href = mkCommandUri('lean4.docView.open', hrefUrl.toString()); + link.attribs.href = mkCommandUri('lean4.docView.openUrl', hrefUrl.toString()); } } } @@ -380,7 +381,7 @@ var side_bar = false; // collapse the side bar menu by default. } /** Called by the user clicking a link. */ - async open(url?: string): Promise { + async open(url?: string | undefined): Promise { if (this.currentURL) { this.backStack.push(this.currentURL); this.forwardStack = []; diff --git a/vscode-lean4/src/exports.ts b/vscode-lean4/src/exports.ts index fe13010ba..807520c2f 100644 --- a/vscode-lean4/src/exports.ts +++ b/vscode-lean4/src/exports.ts @@ -2,12 +2,16 @@ import { InfoProvider } from './infoview' import { DocViewProvider } from './docview'; import { LeanInstaller } from './utils/leanInstaller' import { LeanClientProvider } from './utils/clientProvider'; +import { ProjectInitializationProvider } from './projectinit'; +import { ProjectOperationProvider } from './projectoperations'; export interface Exports { - isLean4Project: boolean; - version: string; - infoProvider: InfoProvider | undefined; - clientProvider: LeanClientProvider | undefined; - installer : LeanInstaller | undefined; - docView : DocViewProvider | undefined; + isLean4Project: boolean + version: string | undefined + infoProvider: InfoProvider | undefined + clientProvider: LeanClientProvider | undefined + projectOperationProvider: ProjectOperationProvider | undefined + installer: LeanInstaller | undefined + docView: DocViewProvider | undefined + projectInitializationProver: ProjectInitializationProvider | undefined } diff --git a/vscode-lean4/src/extension.ts b/vscode-lean4/src/extension.ts index fe69d5c10..e254000de 100644 --- a/vscode-lean4/src/extension.ts +++ b/vscode-lean4/src/extension.ts @@ -1,44 +1,61 @@ -import { window, Uri, workspace, ExtensionContext, TextDocument } from 'vscode' +import { window, ExtensionContext, TextDocument, tasks, commands, Disposable, workspace } from 'vscode' import { AbbreviationFeature } from './abbreviation' import { InfoProvider } from './infoview' -import { DocViewProvider } from './docview'; +import { DocViewProvider } from './docview' import { LeanTaskGutter } from './taskgutter' import { LeanInstaller } from './utils/leanInstaller' -import { LeanpkgService } from './utils/leanpkg'; -import { LeanClientProvider } from './utils/clientProvider'; -import { addDefaultElanPath, removeElanPath, addToolchainBinPath, isElanDisabled, getDefaultLeanVersion} from './config'; -import { findLeanPackageVersionInfo } from './utils/projectInfo'; +import { LeanpkgService } from './utils/leanpkg' +import { LeanClientProvider } from './utils/clientProvider' +import { addDefaultElanPath, removeElanPath, addToolchainBinPath, isElanDisabled, getDefaultLeanVersion, getDefaultElanPath} from './config' +import { findLeanPackageVersionInfo } from './utils/projectInfo' import { Exports } from './exports'; import { logger } from './utils/logger' +import { ProjectInitializationProvider } from './projectinit' +import { ProjectOperationProvider } from './projectoperations' +import { LeanClient } from './leanclient' + +interface AlwaysEnabledFeatures { + docView: DocViewProvider + projectInitializationProvider: ProjectInitializationProvider + installer: LeanInstaller +} + +interface Lean4EnabledFeatures { + clientProvider: LeanClientProvider + infoProvider: InfoProvider + projectOperationProvider: ProjectOperationProvider +} + +async function setLeanFeatureSetActive(isActive: boolean) { + await commands.executeCommand('setContext', 'lean4.isLeanFeatureSetActive', isActive) +} function isLean(languageId : string) : boolean { return languageId === 'lean' || languageId === 'lean4'; } - -function getLeanDocument() : TextDocument | undefined { - let document : TextDocument | undefined; - if (window.activeTextEditor && isLean(window.activeTextEditor.document.languageId)) - { - document = window.activeTextEditor.document +function findOpenLeanDocument() : TextDocument | undefined { + const activeEditor = window.activeTextEditor + if (activeEditor && isLean(activeEditor.document.languageId)) { + return activeEditor.document } - else { - // This happens if vscode starts with a lean file open - // but the "Getting Started" page is active. - for (const editor of window.visibleTextEditors) { - const lang = editor.document.languageId; - if (isLean(lang)) { - document = editor.document; - break; - } + + // This happens if vscode starts with a lean file open + // but the "Getting Started" page is active. + for (const editor of window.visibleTextEditors) { + if (isLean(editor.document.languageId)) { + return editor.document } } - return document; -} -export async function activate(context: ExtensionContext): Promise { + return undefined; +} - // for unit test that tests behavior when there is no elan installed. +/** + * Activates all extension features that are *always* enabled, even when no Lean 4 document is currently open. + */ +function activateAlwaysEnabledFeatures(context: ExtensionContext): AlwaysEnabledFeatures { + // For unit test that tests behavior when there is no elan installed. if (isElanDisabled()) { const elanRoot = removeElanPath(); if (elanRoot){ @@ -48,60 +65,149 @@ export async function activate(context: ExtensionContext): Promise { addDefaultElanPath(); } - const defaultToolchain = getDefaultLeanVersion(); - - // note: workspace.rootPath can be undefined in the untitled or adhoc case - // where the user ran "code lean_filename". - const doc = getLeanDocument(); - let packageUri = null; - let toolchainVersion = null; - if (doc) { - [packageUri, toolchainVersion] = await findLeanPackageVersionInfo(doc.uri); - if (toolchainVersion && toolchainVersion.indexOf('lean:3') > 0) { - logger.log(`Lean4 skipping lean 3 project: ${toolchainVersion}`); - return { isLean4Project: false, version: toolchainVersion, - infoProvider: undefined, clientProvider: undefined, installer: undefined, docView: undefined }; + context.subscriptions.push(commands.registerCommand('lean4.setup.showSetupGuide', async () => { + if (process.platform === 'win32') { + await commands.executeCommand('workbench.action.openWalkthrough', 'leanprover.lean4#guide.windows', false) + } else if (process.platform === 'darwin') { + await commands.executeCommand('workbench.action.openWalkthrough', 'leanprover.lean4#guide.mac', false) + } else if (process.platform === 'linux') { + await commands.executeCommand('workbench.action.openWalkthrough', 'leanprover.lean4#guide.linux', false) + } else { + await commands.executeCommand('workbench.action.openWalkthrough', 'leanprover.lean4#guide.linux', false) } - } + })) + + const docView = new DocViewProvider(context.extensionUri); + context.subscriptions.push(docView); const outputChannel = window.createOutputChannel('Lean: Editor'); + context.subscriptions.push(commands.registerCommand('lean4.troubleshooting.showOutput', () => outputChannel.show(true))) + const projectInitializationProvider = new ProjectInitializationProvider(outputChannel) + context.subscriptions.push(projectInitializationProvider) + + const defaultToolchain = getDefaultLeanVersion(); const installer = new LeanInstaller(outputChannel, defaultToolchain) - context.subscriptions.push(installer); - const versionInfo = await installer.checkLeanVersion(packageUri, toolchainVersion??defaultToolchain) - // Check whether rootPath is a Lean 3 project (the Lean 3 extension also uses the deprecated rootPath) + context.subscriptions.push(commands.registerCommand('lean4.setup.installElan', async () => { + await installer.installElan(); + if (isElanDisabled()) { + addToolchainBinPath(getDefaultElanPath()); + } else { + addDefaultElanPath(); + } + })) + + return { docView, projectInitializationProvider, installer } +} + +async function isLean3Project(installer: LeanInstaller): Promise { + const doc = findOpenLeanDocument(); + + const [packageUri, toolchainVersion] = doc + ? await findLeanPackageVersionInfo(doc.uri) + : [null, null] + + if (toolchainVersion && toolchainVersion.indexOf('lean:3') > 0) { + logger.log(`Lean4 skipping lean 3 project: ${toolchainVersion}`); + return true + } + + const versionInfo = await installer.checkLeanVersion(packageUri, toolchainVersion ?? installer.getDefaultToolchain()) if (versionInfo.version === '3') { - context.subscriptions.pop()?.dispose(); // stop installer - // We need to terminate before registering the LeanClientProvider, - // because that class changes the document id to `lean4`. - return { isLean4Project: false, version: '3', - infoProvider: undefined, clientProvider: undefined, installer: undefined, docView: undefined }; + return true } + return false +} + +function activateAbbreviationFeature(context: ExtensionContext, docView: DocViewProvider): AbbreviationFeature { + const abbrev = new AbbreviationFeature(); + // Pass the abbreviations through to the docView so it can show them on demand. + docView.setAbbreviations(abbrev.abbreviations.symbolsByAbbreviation); + context.subscriptions.push(abbrev); + return abbrev +} + +async function activateLean4Features(context: ExtensionContext, installer: LeanInstaller): Promise { + const clientProvider = new LeanClientProvider(installer, installer.getOutputChannel()); + context.subscriptions.push(clientProvider) + const pkgService = new LeanpkgService() + pkgService.versionChanged(async uri => { + const client: LeanClient | undefined = clientProvider.getClientForFolder(uri) + if (client && !client.isRunning()) { + // This can naturally happen when we update the Lean version using the "Update Dependency" command + // because the Lean server is stopped while doing so. We want to avoid triggering the "Version changed" + // message in this case. + return + } + await installer.handleVersionChanged(uri) + }); + pkgService.lakeFileChanged((uri) => installer.handleLakeFileChanged(uri)); context.subscriptions.push(pkgService); - const leanClientProvider = new LeanClientProvider(installer, pkgService, outputChannel); - context.subscriptions.push(leanClientProvider) + const infoProvider = new InfoProvider(clientProvider, {language: 'lean4'}, context); + context.subscriptions.push(infoProvider) - const info = new InfoProvider(leanClientProvider, {language: 'lean4'}, context); - context.subscriptions.push(info) + context.subscriptions.push(new LeanTaskGutter(clientProvider, context)) - const abbrev = new AbbreviationFeature(); - context.subscriptions.push(abbrev); + const projectOperationProvider: ProjectOperationProvider = new ProjectOperationProvider(installer.getOutputChannel(), clientProvider) - const docView = new DocViewProvider(context.extensionUri); - context.subscriptions.push(docView); + await setLeanFeatureSetActive(true) - // pass the abbreviations through to the docView so it can show them on demand. - docView.setAbbreviations(abbrev.abbreviations.symbolsByAbbreviation); + return { clientProvider, infoProvider, projectOperationProvider } +} - context.subscriptions.push(new LeanTaskGutter(leanClientProvider, context)) +export async function activate(context: ExtensionContext): Promise { + await setLeanFeatureSetActive(false) + const alwaysEnabledFeatures: AlwaysEnabledFeatures = activateAlwaysEnabledFeatures(context) + + if (await isLean3Project(alwaysEnabledFeatures.installer)) { + return { + isLean4Project: false, + version: '3', + infoProvider: undefined, + clientProvider: undefined, + projectOperationProvider: undefined, + installer: alwaysEnabledFeatures.installer, + docView: alwaysEnabledFeatures.docView, + projectInitializationProver: alwaysEnabledFeatures.projectInitializationProvider + } + } - pkgService.versionChanged((uri) => installer.handleVersionChanged(uri)); - pkgService.lakeFileChanged((uri) => installer.handleLakeFileChanged(uri)); + activateAbbreviationFeature(context, alwaysEnabledFeatures.docView) + + if (findOpenLeanDocument()) { + const lean4EnabledFeatures: Lean4EnabledFeatures = await activateLean4Features(context, alwaysEnabledFeatures.installer) + return { + isLean4Project: true, + version: '4', + infoProvider: lean4EnabledFeatures.infoProvider, + clientProvider: lean4EnabledFeatures.clientProvider, + projectOperationProvider: lean4EnabledFeatures.projectOperationProvider, + installer: alwaysEnabledFeatures.installer, + docView: alwaysEnabledFeatures.docView, + projectInitializationProver: alwaysEnabledFeatures.projectInitializationProvider + } + } - return { isLean4Project: true, version: '4', - infoProvider: info, clientProvider: leanClientProvider, installer, docView}; + // No Lean 4 document yet => Load remaining features when one is open + const disposeActivationListener: Disposable = workspace.onDidOpenTextDocument(async doc => { + if (isLean(doc.languageId)) { + await activateLean4Features(context, alwaysEnabledFeatures.installer) + disposeActivationListener.dispose() + } + }, context.subscriptions) + + return { + isLean4Project: true, + version: '4', + infoProvider: undefined, + clientProvider: undefined, + projectOperationProvider: undefined, + installer: alwaysEnabledFeatures.installer, + docView: alwaysEnabledFeatures.docView, + projectInitializationProver: alwaysEnabledFeatures.projectInitializationProvider + } } diff --git a/vscode-lean4/src/infoview.ts b/vscode-lean4/src/infoview.ts index 0fbe22fdf..4d7bf1ff9 100644 --- a/vscode-lean4/src/infoview.ts +++ b/vscode-lean4/src/infoview.ts @@ -281,7 +281,7 @@ export class InfoProvider implements Disposable { await this.sendPosition(); }), commands.registerTextEditorCommand('lean4.displayGoal', (editor) => this.openPreview(editor)), - commands.registerTextEditorCommand('lean4.toggleInfoview', (editor) => this.toggleInfoview(editor)), + commands.registerCommand('lean4.toggleInfoview', () => this.toggleInfoview()), commands.registerTextEditorCommand('lean4.displayList', async (editor) => { await this.openPreview(editor); await this.webviewPanel?.api.requestedAction({kind: 'toggleAllMessages'}); @@ -491,12 +491,14 @@ export class InfoProvider implements Disposable { this.rpcSessions = remaining } - private async toggleInfoview(editor: TextEditor) { + private async toggleInfoview() { if (this.webviewPanel) { this.webviewPanel.dispose(); // the onDispose handler sets this.webviewPanel = undefined + } else if (window.activeTextEditor && window.activeTextEditor.document.languageId === 'lean4') { + await this.openPreview(window.activeTextEditor); } else { - return this.openPreview(editor); + void window.showErrorMessage('No active Lean editor tab. Make sure to focus the Lean editor tab for which you want to open the infoview.') } } diff --git a/vscode-lean4/src/leanclient.ts b/vscode-lean4/src/leanclient.ts index c144481a5..90915c566 100644 --- a/vscode-lean4/src/leanclient.ts +++ b/vscode-lean4/src/leanclient.ts @@ -1,12 +1,11 @@ import { TextDocument, EventEmitter, Diagnostic, DocumentHighlight, Range, DocumentHighlightKind, workspace, Disposable, Uri, ConfigurationChangeEvent, OutputChannel, DiagnosticCollection, - WorkspaceFolder, window, commands } from 'vscode' + WorkspaceFolder, window, ProgressLocation, ProgressOptions, Progress } from 'vscode' import { DiagnosticSeverity, DidChangeTextDocumentParams, DidCloseTextDocumentParams, - DidOpenTextDocumentNotification, DocumentFilter, InitializeResult, LanguageClient, @@ -21,7 +20,7 @@ import * as ls from 'vscode-languageserver-protocol' import { toolchainPath, lakePath, addServerEnvPaths, serverArgs, serverLoggingEnabled, serverLoggingPath, shouldAutofocusOutput, getElaborationDelay, lakeEnabled, automaticallyBuildDependencies } from './config' import { assert } from './utils/assert' import { LeanFileProgressParams, LeanFileProgressProcessingInfo, ServerStoppedReason } from '@leanprover/infoview-api'; -import { batchExecute } from './utils/batch' +import { ExecutionExitCode, ExecutionResult, batchExecute } from './utils/batch' import { readLeanVersion } from './utils/projectInfo'; import * as fs from 'fs'; import { URL } from 'url'; @@ -31,6 +30,7 @@ import { logger } from './utils/logger' import { SemVer } from 'semver'; import { fileExists, isFileInFolder } from './utils/fsHelper'; import { c2pConverter, p2cConverter, patchConverters } from './utils/converters' +import { displayErrorWithOutput } from './utils/errors' import path = require('path') const escapeRegExp = (s: string) => s.replace(/[.*+?^${}()|[\]\\]/g, '\\$&'); @@ -47,11 +47,12 @@ export class LeanClient implements Disposable { private toolchainPath: string private outputChannel: OutputChannel; private workspaceFolder: WorkspaceFolder | undefined; - private folderUri: Uri; + folderUri: Uri; private subscriptions: Disposable[] = [] private noPrompt : boolean = false; private showingRestartMessage : boolean = false; private elanDefaultToolchain: string; + private isRestarting: boolean = false private didChangeEmitter = new EventEmitter() didChange = this.didChangeEmitter.event @@ -141,211 +142,67 @@ export class LeanClient implements Disposable { } async showRestartMessage(restartFile: boolean = false): Promise { - if (!this.showingRestartMessage) { - this.showingRestartMessage = true; - let restartItem :string; - let messageTitle :string; - if (!restartFile) { - restartItem = 'Restart Lean Server'; - messageTitle = 'Lean Server has stopped unexpectedly.' + if (this.showingRestartMessage) { + return + } + this.showingRestartMessage = true; + let restartItem: string; + let messageTitle: string; + if (!restartFile) { + restartItem = 'Restart Lean Server'; + messageTitle = 'Lean Server has stopped unexpectedly.' + } else { + restartItem = 'Restart Lean Server on this file'; + messageTitle = 'The Lean Server has stopped processing this file.' + } + const item = await window.showErrorMessage(messageTitle, restartItem) + this.showingRestartMessage = false; + if (item === restartItem) { + if (restartFile && window.activeTextEditor) { + await this.restartFile(window.activeTextEditor.document); } else { - restartItem = 'Restart Lean Server on this file'; - messageTitle = 'The Lean Server has stopped processing this file.' - } - const item = await window.showErrorMessage(messageTitle, restartItem) - this.showingRestartMessage = false; - if (item === restartItem) { - if (restartFile && window.activeTextEditor){ - await this.restartFile(window.activeTextEditor.document); - } else { - void this.start(); - } + void this.start(); } } } async restart(): Promise { - const startTime = Date.now() - - logger.log('[LeanClient] Restarting Lean Server') - if (this.isStarted()) { - await this.stop() - } - - this.restartingEmitter.fire(undefined) - this.toolchainPath = toolchainPath(); - let version: string | null = null; - const env = addServerEnvPaths(process.env); - if (serverLoggingEnabled()) { - env.LEAN_SERVER_LOG_DIR = serverLoggingPath() - } - - let executable = lakePath() || - (this.toolchainPath ? join(this.toolchainPath, 'bin', 'lake') : 'lake'); - - // check if the lake process will start (skip it on scheme: 'untitled' files) - let useLake = lakeEnabled() && this.folderUri && this.folderUri.scheme === 'file'; - if (useLake) { - let knownDate = false; - const lakefile = Uri.joinPath(this.folderUri, 'lakefile.lean') - if (!await fileExists(new URL(lakefile.toString()))) { - useLake = false; - } - else { - // see if we can avoid the more expensive checkLakeVersion call. - const date = await this.checkToolchainVersion(this.folderUri); - if (date){ - // Feb 16 2022 is when the 3.1.0.pre was released. - useLake = date >= new Date(2022, 1, 16); - knownDate = true; - } - if (useLake && !knownDate){ - useLake = await this.checkLakeVersion(executable, version); - } - } - } - - if (!useLake) { - executable = (this.toolchainPath) ? join(this.toolchainPath, 'bin', 'lean') : 'lean'; - } - - const cwd = this.folderUri?.fsPath - if (!cwd && !version){ - // Fixes issue #227, for adhoc files it would pick up the cwd from the open folder - // which is not what we want. For adhoc files we want the (default) toolchain instead. - version = this.elanDefaultToolchain; - } - - let options = version ? ['+' + version] :[] - if (useLake) { - options = options.concat(['serve', '--']) - } else{ - options = options.concat(['--server']) - } - - // Add folder name to command-line so that it shows up in `ps aux`. - if (cwd) { - options.push('' + cwd) - } else { - options.push('untitled') + if (this.isRestarting) { + await window.showErrorMessage('Client is already being started.') + return } - - const serverOptions: ServerOptions = { - command: executable, - args: options.concat(serverArgs()), - options: { - cwd, - env + this.isRestarting = true + try { + logger.log('[LeanClient] Restarting Lean Server') + if (this.isStarted()) { + await this.stop() } - } - const documentSelector: DocumentFilter = { - language: 'lean4' - } + this.restartingEmitter.fire(undefined) + this.toolchainPath = toolchainPath(); - if (this.folderUri){ - documentSelector.scheme = this.folderUri.scheme - if (this.folderUri.scheme !== 'untitled') { - documentSelector.pattern = `${this.folderUri.fsPath}/**/*` + const progressOptions: ProgressOptions = { + location: ProgressLocation.Notification, + title: 'Starting Lean language client', + cancellable: false } + await window.withProgress(progressOptions, async progress => + await this.startClient(progress)) + } finally { + this.isRestarting = false } + } - const clientOptions: LanguageClientOptions = { - outputChannel: this.outputChannel, - revealOutputChannelOn: RevealOutputChannelOn.Never, // contrary to the name, this disables the message boxes - documentSelector: [documentSelector], - workspaceFolder: this.workspaceFolder, - initializationOptions: { - editDelay: getElaborationDelay(), hasWidgets: true, - }, - connectionOptions: { - maxRestartCount: 0, - cancellationStrategy: undefined as any, - }, - middleware: { - handleDiagnostics: (uri, diagnostics, next) => { - next(uri, diagnostics); - if (!this.client) return; - const uri_ = c2pConverter.asUri(uri); - const diagnostics_ = []; - for (const d of diagnostics) { - const d_: ls.Diagnostic = { - ...c2pConverter.asDiagnostic(d), - }; - diagnostics_.push(d_); - } - this.diagnosticsEmitter.fire({uri: uri_, diagnostics: diagnostics_}); - }, - - didOpen: async () => { - // Note: as per the LSP spec: An open notification must not be sent more than once - // without a corresponding close notification send before. This means open and close - // notification must be balanced and the max open count for a particular textDocument - // is one. So this even does nothing the notification is handled by the - // openLean4Document method below after the 'lean4' languageId is established and - // it has weeded out documents opened to invisible editors (like 'git:' schemes and - // invisible editors created for Ctrl+Hover events. A side effect of unbalanced - // open/close notification is leaking 'lean --worker' processes. - // See https://github.com/microsoft/vscode/issues/78453). - return; - }, - - didChange: async (data, next) => { - await next(data); - if (!this.running || !this.client) return; // there was a problem starting lean server. - const params = c2pConverter.asChangeTextDocumentParams(data); - this.didChangeEmitter.fire(params); - }, - - didClose: async (doc, next) => { - if (!this.isOpen.delete(doc.uri.toString())) { - return; - } - await next(doc); - if (!this.running || !this.client) return; // there was a problem starting lean server. - const params = c2pConverter.asCloseTextDocumentParams(doc); - this.didCloseEmitter.fire(params); - }, - - provideDocumentHighlights: async (doc, pos, ctok, next) => { - const leanHighlights = await next(doc, pos, ctok); - if (leanHighlights?.length) return leanHighlights; - - // vscode doesn't fall back to textual highlights, - // so we need to do that manually - await new Promise((res) => setTimeout(res, 250)); - if (ctok.isCancellationRequested) return; - - const wordRange = doc.getWordRangeAtPosition(pos); - if (!wordRange) return; - const word = doc.getText(wordRange); + private async startClient(progress: Progress<{ message?: string; increment?: number }>) { + // Should only be called from `restart` - const highlights: DocumentHighlight[] = []; - const text = doc.getText(); - const nonWordPattern = '[`~@$%^&*()-=+\\[{\\]}⟨⟩⦃⦄⟦⟧⟮⟯‹›\\\\|;:\",./\\s]|^|$' - const regexp = new RegExp(`(?<=${nonWordPattern})${escapeRegExp(word)}(?=${nonWordPattern})`, 'g') - for (const match of text.matchAll(regexp)) { - const start = doc.positionAt(match.index ?? 0) - highlights.push({ - range: new Range(start, start.translate(0, match[0].length)), - kind: DocumentHighlightKind.Text, - }) - } + const startTime = Date.now() + progress.report({ increment: 0 }) + this.client = await this.setupClient() - return highlights; - } - }, - } - this.client = new LanguageClient( - 'lean4', - 'Lean 4', - serverOptions, - clientOptions - ) let insideRestart = true; - patchConverters(this.client.protocol2CodeConverter, this.client.code2ProtocolConverter) try { - this.client.onDidChangeState(async (s) => { + this.client.onDidChangeState(async s => { // see https://github.com/microsoft/vscode-languageserver-node/issues/825 if (s.newState === State.Starting) { logger.log('[LeanClient] starting'); @@ -359,7 +216,7 @@ export class LeanClient implements Disposable { } else if (s.newState === State.Stopped) { this.running = false; logger.log('[LeanClient] has stopped or it failed to start'); - if (!this.noPrompt){ + if (!this.noPrompt) { // only raise this event and show the message if we are not the ones // who called the stop() method. this.stoppedEmitter.fire({message:'Lean server has stopped.', reason:''}); @@ -367,6 +224,7 @@ export class LeanClient implements Disposable { } } }) + progress.report({ increment: 80 }) await this.client.start() // tell the new client about the documents that are already open! for (const key of this.isOpen.keys()) { @@ -406,16 +264,12 @@ export class LeanClient implements Disposable { // Reveal the standard error output channel when the server prints something to stderr. // The vscode-languageclient library already takes care of writing it to the output channel. let stderrMsgBoxVisible = false; - (this.client as any)._serverProcess.stderr.on('data', async (chunk : Buffer) => { + (this.client as any)._serverProcess.stderr.on('data', async (chunk: Buffer) => { if (shouldAutofocusOutput()) { this.client?.outputChannel.show(true); } else if (!stderrMsgBoxVisible) { stderrMsgBoxVisible = true; - const outputItem = 'Show stderr output'; - const outPrompt = `Lean server printed an error:\n${chunk.toString()}`; - if (await window.showErrorMessage(outPrompt, outputItem) === outputItem) { - this.outputChannel.show(false); - } + await displayErrorWithOutput(`Lean server printed an error:\n${chunk.toString()}`) stderrMsgBoxVisible = false; } }); @@ -424,6 +278,24 @@ export class LeanClient implements Disposable { insideRestart = false; } + async withStoppedClient(action: () => Promise): Promise<'Success' | 'IsRestarting'> { + if (this.isRestarting) { + return 'IsRestarting' + } + this.isRestarting = true // Ensure that client cannot be restarted in the mean-time + + if (this.isStarted()) { + await this.stop() + } + + await action() + + this.isRestarting = false + await this.restart() + + return 'Success' + } + async openLean4Document(doc: TextDocument) { if (this.isOpen.has(doc.uri.toString())) return; if (!await this.isSameWorkspace(doc.uri)){ @@ -469,7 +341,6 @@ export class LeanClient implements Disposable { else { return uri.scheme === 'untitled' } - return false; } getWorkspaceFolder() : string { @@ -602,8 +473,12 @@ export class LeanClient implements Disposable { // Check that the Lake version is high enough to support "lake serve" option. const versionOptions = version ? ['+' + version, '--version'] : ['--version'] const start = Date.now() - const lakeVersion = await batchExecute(executable, versionOptions, this.folderUri?.fsPath, undefined); + const result: ExecutionResult = await batchExecute(executable, versionOptions, this.folderUri?.fsPath); + if (result.exitCode !== ExecutionExitCode.Success) { + return false + } logger.log(`[LeanClient] Ran '${executable} ${versionOptions.join(' ')}' in ${Date.now() - start} ms`); + const lakeVersion = result.stdout const actual = this.extractVersion(lakeVersion) if (actual.compare('3.0.0') > 0) { return true; @@ -623,4 +498,182 @@ export class LeanClient implements Disposable { return new SemVer('0.0.0'); } } + + private async determineServerOptions(): Promise { + const env = addServerEnvPaths(process.env) + if (serverLoggingEnabled()) { + env.LEAN_SERVER_LOG_DIR = serverLoggingPath() + } + + const [serverExecutable, options] = await this.determineExecutable() + + const cwd = this.folderUri?.fsPath + if (cwd) { + // Add folder name to command-line so that it shows up in `ps aux`. + options.push(cwd) + } else { + // Fixes issue #227, for adhoc files it would pick up the cwd from the open folder + // which is not what we want. For adhoc files we want the (default) toolchain instead. + options.unshift('+' + this.elanDefaultToolchain) + options.push('untitled') + } + + return { + command: serverExecutable, + args: options.concat(serverArgs()), + options: { + cwd, + env + } + } + } + + private async determineExecutable(): Promise<[string, string[]]> { + const lakeExecutable = lakePath() || + (this.toolchainPath ? join(this.toolchainPath, 'bin', 'lake') : 'lake') + const leanExecutable = + (this.toolchainPath) ? join(this.toolchainPath, 'bin', 'lean') : 'lean' + + if (await this.shouldUseLake(lakeExecutable)) { + return [lakeExecutable, ['serve', '--']] + } else{ + return [leanExecutable, ['--server']] + } + } + + private async shouldUseLake(lakeExecutable: string): Promise { + // check if the lake process will start (skip it on scheme: 'untitled' files) + if (!lakeEnabled() || !this.folderUri || this.folderUri.scheme !== 'file') { + return false + } + + const lakefile = Uri.joinPath(this.folderUri, 'lakefile.lean') + if (!await fileExists(new URL(lakefile.toString()))) { + return false + } + + // see if we can avoid the more expensive checkLakeVersion call. + const date = await this.checkToolchainVersion(this.folderUri); + if (date) { + // Feb 16 2022 is when the 3.1.0.pre was released. + return date >= new Date(2022, 1, 16); + } + + return await this.checkLakeVersion(lakeExecutable, null); + } + + private obtainClientOptions(): LanguageClientOptions { + const documentSelector: DocumentFilter = { + language: 'lean4' + } + + if (this.folderUri){ + documentSelector.scheme = this.folderUri.scheme + if (this.folderUri.scheme !== 'untitled') { + documentSelector.pattern = `${this.folderUri.fsPath}/**/*` + } + } + + return { + outputChannel: this.outputChannel, + revealOutputChannelOn: RevealOutputChannelOn.Never, // contrary to the name, this disables the message boxes + documentSelector: [documentSelector], + workspaceFolder: this.workspaceFolder, + initializationOptions: { + editDelay: getElaborationDelay(), hasWidgets: true, + }, + connectionOptions: { + maxRestartCount: 0, + cancellationStrategy: undefined as any, + }, + middleware: { + handleDiagnostics: (uri, diagnostics, next) => { + next(uri, diagnostics); + if (!this.client) return; + const uri_ = c2pConverter.asUri(uri); + const diagnostics_ = []; + for (const d of diagnostics) { + const d_: ls.Diagnostic = { + ...c2pConverter.asDiagnostic(d), + }; + diagnostics_.push(d_); + } + this.diagnosticsEmitter.fire({uri: uri_, diagnostics: diagnostics_}); + }, + + didOpen: async () => { + // Note: as per the LSP spec: An open notification must not be sent more than once + // without a corresponding close notification send before. This means open and close + // notification must be balanced and the max open count for a particular textDocument + // is one. So this even does nothing the notification is handled by the + // openLean4Document method below after the 'lean4' languageId is established and + // it has weeded out documents opened to invisible editors (like 'git:' schemes and + // invisible editors created for Ctrl+Hover events. A side effect of unbalanced + // open/close notification is leaking 'lean --worker' processes. + // See https://github.com/microsoft/vscode/issues/78453). + return; + }, + + didChange: async (data, next) => { + await next(data); + if (!this.running || !this.client) return; // there was a problem starting lean server. + const params = c2pConverter.asChangeTextDocumentParams(data); + this.didChangeEmitter.fire(params); + }, + + didClose: async (doc, next) => { + if (!this.isOpen.delete(doc.uri.toString())) { + return; + } + await next(doc); + if (!this.running || !this.client) return; // there was a problem starting lean server. + const params = c2pConverter.asCloseTextDocumentParams(doc); + this.didCloseEmitter.fire(params); + }, + + provideDocumentHighlights: async (doc, pos, ctok, next) => { + const leanHighlights = await next(doc, pos, ctok); + if (leanHighlights?.length) return leanHighlights; + + // vscode doesn't fall back to textual highlights, + // so we need to do that manually + await new Promise((res) => setTimeout(res, 250)); + if (ctok.isCancellationRequested) return; + + const wordRange = doc.getWordRangeAtPosition(pos); + if (!wordRange) return; + const word = doc.getText(wordRange); + + const highlights: DocumentHighlight[] = []; + const text = doc.getText(); + const nonWordPattern = '[`~@$%^&*()-=+\\[{\\]}⟨⟩⦃⦄⟦⟧⟮⟯‹›\\\\|;:\",./\\s]|^|$' + const regexp = new RegExp(`(?<=${nonWordPattern})${escapeRegExp(word)}(?=${nonWordPattern})`, 'g') + for (const match of text.matchAll(regexp)) { + const start = doc.positionAt(match.index ?? 0) + highlights.push({ + range: new Range(start, start.translate(0, match[0].length)), + kind: DocumentHighlightKind.Text, + }) + } + + return highlights; + } + }, + } + } + + private async setupClient(): Promise { + const serverOptions: ServerOptions = await this.determineServerOptions() + const clientOptions: LanguageClientOptions = this.obtainClientOptions() + + const client = new LanguageClient( + 'lean4', + 'Lean 4', + serverOptions, + clientOptions + ) + + patchConverters(client.protocol2CodeConverter, client.code2ProtocolConverter) + return client + } } diff --git a/vscode-lean4/src/projectinit.ts b/vscode-lean4/src/projectinit.ts new file mode 100644 index 000000000..c7c95d580 --- /dev/null +++ b/vscode-lean4/src/projectinit.ts @@ -0,0 +1,208 @@ +import { Disposable, Uri, commands, window, workspace, SaveDialogOptions, OutputChannel } from 'vscode'; +import path = require('path'); +import { checkParentFoldersForLeanProject, isValidLeanProject } from './utils/projectInfo'; +import { elanSelfUpdate } from './utils/elan'; +import { lake } from './utils/lake'; +import { ExecutionExitCode, ExecutionResult, batchExecuteWithProgress, displayError } from './utils/batch'; + +export class ProjectInitializationProvider implements Disposable { + + private subscriptions: Disposable[] = []; + + constructor(private channel: OutputChannel) { + this.subscriptions.push( + commands.registerCommand('lean4.project.createStandaloneProject', () => this.createStandaloneProject()), + commands.registerCommand('lean4.project.createMathlibProject', () => this.createMathlibProject()), + commands.registerCommand('lean4.project.open', () => this.openProject()), + commands.registerCommand('lean4.project.clone', () => this.cloneProject()) + ) + } + + private async createStandaloneProject() { + const projectFolder: Uri | 'DidNotComplete' = await this.createProject() + + if (projectFolder !== 'DidNotComplete') { + await ProjectInitializationProvider.openNewFolder(projectFolder) + } + } + + private async createMathlibProject() { + const mathlibToolchain = 'leanprover-community/mathlib4:lean-toolchain' + const projectFolder: Uri | 'DidNotComplete' = await this.createProject('math', mathlibToolchain) + if (projectFolder === 'DidNotComplete') { + return + } + + const cacheGetResult: ExecutionResult = await lake(this.channel, projectFolder, mathlibToolchain).fetchMathlibCache() + if (cacheGetResult.exitCode === ExecutionExitCode.Cancelled) { + return + } + if (cacheGetResult.exitCode !== ExecutionExitCode.Success) { + await displayError(cacheGetResult, 'Cannot fetch Mathlib build artifact cache.') + return + } + + await ProjectInitializationProvider.openNewFolder(projectFolder) + } + + private async createProject( + kind?: string | undefined, + toolchain: string = 'leanprover/lean4:stable'): Promise { + + const projectFolder: Uri | undefined = await ProjectInitializationProvider.askForNewProjectFolderLocation({ + saveLabel: 'Create project folder', + title: 'Create a new project folder' + }) + if (projectFolder === undefined) { + return 'DidNotComplete' + } + + await workspace.fs.createDirectory(projectFolder) + + // This can fail silently in setups without Elan. + await elanSelfUpdate(this.channel) + + const projectName: string = path.basename(projectFolder.fsPath) + const result: ExecutionResult = await lake(this.channel, projectFolder, toolchain).initProject(projectName, kind) + if (result.exitCode !== ExecutionExitCode.Success) { + await displayError(result, 'Cannot initialize project.') + return 'DidNotComplete' + } + + const updateResult: ExecutionResult = await lake(this.channel, projectFolder, toolchain).updateDependencies() + if (updateResult.exitCode === ExecutionExitCode.Cancelled) { + return 'DidNotComplete' + } + if (updateResult.exitCode !== ExecutionExitCode.Success) { + await displayError(updateResult, 'Cannot update dependencies.') + return 'DidNotComplete' + } + + return projectFolder + } + + private async openProject() { + const projectFolders: Uri[] | undefined = await window.showOpenDialog({ + title: 'Open Lean 4 project folder containing a \'lean-toolchain\' file', + openLabel: 'Open project folder', + canSelectFiles: false, + canSelectFolders: true, + canSelectMany: false + }) + if (projectFolders === undefined || projectFolders.length !== 1) { + return + } + + let projectFolder = projectFolders[0] + if (!await ProjectInitializationProvider.checkIsFileUriOrShowError(projectFolder)) { + return + } + + if (!await isValidLeanProject(projectFolder)) { + const parentProjectFolder: Uri | undefined = await ProjectInitializationProvider.attemptFindingLeanProjectInParentFolder(projectFolder) + if (parentProjectFolder === undefined) { + return + } + projectFolder = parentProjectFolder + } + + // This kills the extension host, so it has to be the last command + await commands.executeCommand('vscode.openFolder', projectFolder) + } + + private static async attemptFindingLeanProjectInParentFolder(projectFolder: Uri): Promise { + const parentProjectFolder: Uri | undefined = await checkParentFoldersForLeanProject(projectFolder) + if (parentProjectFolder === undefined) { + void window.showErrorMessage('The selected folder is not a valid Lean 4 project folder. Please make sure to select a folder containing a \'lean-toolchain\' file.') + return undefined + } + + const message = `The selected folder is not a valid Lean 4 project folder because it does not contain a 'lean-toolchain' file. +However, a valid Lean 4 project folder was found in one of the parent directories at '${parentProjectFolder.fsPath}'. +Open this project instead?` + const input = 'Open parent directory project' + const choice: string | undefined = await window.showInformationMessage(message, { modal: true }, input) + if (choice !== input) { + return undefined + } + + return parentProjectFolder + } + + private async cloneProject() { + const unparsedProjectUri: string | undefined = await window.showInputBox({ + title: 'URL Input', + value: 'https://github.com/leanprover-community/mathlib4', + prompt: 'URL of Git repository for existing Lean 4 project', + validateInput: value => { + try { + Uri.parse(value, true) + return undefined // Valid URI + } catch (e) { + return 'Invalid URL' + } + } + }) + if (unparsedProjectUri === undefined) { + return + } + const existingProjectUri = Uri.parse(unparsedProjectUri) + + const projectFolder: Uri | undefined = await ProjectInitializationProvider.askForNewProjectFolderLocation({ + saveLabel: 'Create project folder', + title: 'Create a new project folder to clone existing Lean 4 project into' + }) + if (projectFolder === undefined) { + return + } + + const result: ExecutionResult = await batchExecuteWithProgress('git', ['clone', existingProjectUri.toString(), projectFolder.fsPath], 'Cloning project', { channel: this.channel, allowCancellation: true }) + if (result.exitCode === ExecutionExitCode.Cancelled) { + return + } + if (result.exitCode !== ExecutionExitCode.Success) { + await displayError(result, 'Cannot download project.') + return + } + + // Try it. If this is not a mathlib project, it will fail silently. Otherwise, it will grab the cache. + const fetchResult: ExecutionResult = await lake(this.channel, projectFolder).fetchMathlibCache(true) + if (fetchResult.exitCode === ExecutionExitCode.Cancelled) { + return + } + + await ProjectInitializationProvider.openNewFolder(projectFolder) + } + + private static async askForNewProjectFolderLocation(options: SaveDialogOptions): Promise { + const projectFolder: Uri | undefined = await window.showSaveDialog(options) + if (projectFolder === undefined || !await this.checkIsFileUriOrShowError(projectFolder)) { + return undefined + } + return projectFolder + } + + private static async checkIsFileUriOrShowError(projectFolder: Uri): Promise { + if (projectFolder.scheme === 'file') { + return true + } else { + void window.showErrorMessage('Project folder must be created in a file system.') + return false + } + } + + private static async openNewFolder(projectFolder: Uri) { + const message = `Project initialized. Open new project folder '${path.basename(projectFolder.fsPath)}'?` + const input = 'Open project folder' + const choice: string | undefined = await window.showInformationMessage(message, { modal: true }, input) + if (choice === input) { + // This kills the extension host, so it has to be the last command + await commands.executeCommand('vscode.openFolder', projectFolder) + } + } + + dispose() { + for (const s of this.subscriptions) { s.dispose(); } + } + +} diff --git a/vscode-lean4/src/projectoperations.ts b/vscode-lean4/src/projectoperations.ts new file mode 100644 index 000000000..f46a078aa --- /dev/null +++ b/vscode-lean4/src/projectoperations.ts @@ -0,0 +1,341 @@ +import { Disposable, commands, window, OutputChannel, QuickPickItem, Uri } from 'vscode'; +import { LakeRunner, cacheNotFoundError, lake } from './utils/lake'; +import { ExecutionExitCode, ExecutionResult, batchExecute, displayError } from './utils/batch'; +import { LeanClientProvider } from './utils/clientProvider'; +import { LeanClient } from './leanclient'; +import { join } from 'path'; +import * as fs from 'fs' +import { DirectGitDependency, Manifest, ManifestReadError, parseAsManifest, parseManifestInFolder } from './utils/manifest'; + +export class ProjectOperationProvider implements Disposable { + + private subscriptions: Disposable[] = [] + private isRunningOperation: boolean = false // Used to synchronize project operations + + constructor(private channel: OutputChannel, private clientProvider: LeanClientProvider) { + this.subscriptions.push( + commands.registerCommand('lean4.project.build', () => this.buildProject()), + commands.registerCommand('lean4.project.clean', () => this.cleanProject()), + commands.registerCommand('lean4.project.updateDependency', () => this.updateDependency()), + commands.registerCommand('lean4.project.fetchCache', () => this.fetchMathlibCache()) + ) + } + + private async buildProject() { + await this.runOperation(async lakeRunner => { + const fetchResult: 'Success' | 'CacheNotAvailable' | 'Cancelled' = await this.tryFetchingCache(lakeRunner) + if (fetchResult === 'Cancelled') { + return + } + + const result: ExecutionResult = await lakeRunner.build() + if (result.exitCode === ExecutionExitCode.Cancelled) { + return + } + if (result.exitCode !== ExecutionExitCode.Success) { + void displayError(result, 'Cannot build project.') + return + } + + void window.showInformationMessage('Project built successfully.') + return + }) + } + + private async cleanProject() { + const deleteInput = 'Proceed' + const deleteChoice: string | undefined = await window.showInformationMessage('Delete all build artifacts?', { modal: true }, deleteInput) + if (deleteChoice !== deleteInput) { + return + } + + await this.runOperation(async lakeRunner => { + const cleanResult: ExecutionResult = await lakeRunner.clean() + if (cleanResult.exitCode === ExecutionExitCode.Cancelled) { + return + } + if (cleanResult.exitCode !== ExecutionExitCode.Success) { + void displayError(cleanResult, 'Cannot delete build artifacts.') + return + } + + const checkResult: 'Yes' | 'No' | 'Cancelled' = await lakeRunner.isMathlibCacheGetAvailable() + if (checkResult === 'Cancelled') { + return + } + if (checkResult === 'No') { + void window.showInformationMessage('Project cleaned successfully.') + return + } + + const fetchMessage = 'Project cleaned successfully. Do you want to fetch Mathlib\'s build artifact cache?' + const fetchInput = 'Fetch Cache' + const fetchChoice: string | undefined = await window.showInformationMessage(fetchMessage, { modal: true }, fetchInput) + if (fetchChoice !== fetchInput) { + return + } + + const fetchResult: ExecutionResult = await lakeRunner.fetchMathlibCache() + if (fetchResult.exitCode === ExecutionExitCode.Cancelled) { + return + } + if (fetchResult.exitCode !== ExecutionExitCode.Success) { + void displayError(fetchResult, 'Cannot fetch Mathlib build artifact cache.') + return + } + void window.showInformationMessage('Mathlib build artifact cache fetched successfully.') + }) + } + + private async fetchMathlibCache() { + await this.runOperation(async lakeRunner => { + const result: ExecutionResult = await lakeRunner.fetchMathlibCache() + if (result.exitCode === ExecutionExitCode.Cancelled) { + return + } + if (result.exitCode !== ExecutionExitCode.Success) { + if (result.stderr.includes(cacheNotFoundError)) { + void window.showErrorMessage('This command cannot be used in non-Mathlib projects.') + return + } + void displayError(result, 'Cannot fetch Mathlib build artifact cache.') + return + } + + void window.showInformationMessage('Mathlib build artifact cache fetched successfully.') + }) + } + + private async updateDependency() { + if (!window.activeTextEditor) { + return + } + + const activeClient: LeanClient | undefined = this.clientProvider.getActiveClient() + if (!activeClient) { + void window.showErrorMessage('No active client.') + this.isRunningOperation = false + return + } + + const manifestResult: Manifest | ManifestReadError = await parseManifestInFolder(activeClient.folderUri) + if (typeof manifestResult === 'string') { + void window.showErrorMessage(manifestResult) + return + } + + const dependencies: (DirectGitDependency & { remoteRevision?: string | undefined })[] = + await this.findUpdateableDependencies(manifestResult.directGitDependencies) + if (dependencies.length === 0) { + void window.showInformationMessage('Nothing to update - all dependencies are up-to-date.') + return + } + + const items: GitDependencyQuickPickItem[] = dependencies.map(gitDep => { + const shortLocalRevision: string = gitDep.revision.substring(0, 7) + const shortRemoteRevision: string | undefined = gitDep.remoteRevision?.substring(0, 7) + + const detail: string = shortRemoteRevision + ? `Current: ${shortLocalRevision} ⟹ New: ${shortRemoteRevision}` + : `Current: ${shortLocalRevision}` + + return { + label: `${gitDep.name} @ ${gitDep.inputRevision}`, + description: gitDep.uri.toString(), + detail, + ...gitDep + } + }) + + const dependencyChoice: GitDependencyQuickPickItem | undefined = await window.showQuickPick(items, { + title: 'Choose a dependency to update', + canPickMany: false + }) + if (!dependencyChoice) { + return + } + + const localToolchainPath: string = join(activeClient.folderUri.fsPath, 'lean-toolchain') + const dependencyToolchainResult: string | 'DoNotUpdate' | 'Cancelled' = await this.determineDependencyToolchain(localToolchainPath, dependencyChoice) + if (dependencyToolchainResult === 'Cancelled') { + return + } + + await this.runOperation(async lakeRunner => { + if (dependencyToolchainResult !== 'DoNotUpdate') { + try { + fs.writeFileSync(localToolchainPath, dependencyToolchainResult) + } catch { + void window.showErrorMessage('Cannot update Lean version.') + return + } + } + + const result: ExecutionResult = await lakeRunner.updateDependency(dependencyChoice.name) + if (result.exitCode === ExecutionExitCode.Cancelled) { + return + } + if (result.exitCode !== ExecutionExitCode.Success) { + void displayError(result, 'Cannot update dependency.') + return + } + + await this.tryFetchingCache(lakeRunner) + }) + } + + private async findUpdateableDependencies(dependencies: DirectGitDependency[]) { + const augmented: (DirectGitDependency & { remoteRevision?: string | undefined })[] = [] + + for (const dependency of dependencies) { + const result: ExecutionResult = await batchExecute('git', ['ls-remote', dependency.uri.toString(), dependency.inputRevision]) + if (result.exitCode !== ExecutionExitCode.Success) { + augmented.push(dependency) + continue + } + + const matches: RegExpMatchArray | null = result.stdout.match(/^[a-z0-9]+/) + if (!matches) { + augmented.push(dependency) + continue + } + + const remoteRevision: string = matches[0] + if (dependency.revision === remoteRevision) { + // Cannot be updated - filter it + continue + } + + augmented.push({ remoteRevision, ...dependency }) + } + + return augmented + } + + private async determineDependencyToolchain(localToolchainPath: string, dependency: DirectGitDependency): Promise { + const dependencyToolchainUri: Uri | undefined = this.determineDependencyToolchainUri(dependency.uri, dependency.inputRevision) + if (!dependencyToolchainUri) { + const message = `Could not determine Lean version of ${dependency.name} at ${dependency.uri}, as doing so is currently only supported for GitHub projects. Do you want to update ${dependency.name} without updating the Lean version of the open project to that of ${dependency.name} regardless?` + const input = 'Proceed' + const choice: string | undefined = await window.showInformationMessage(message, { modal: true}, input) + return choice === 'input' ? 'DoNotUpdate' : 'Cancelled' + } + + const toolchainResult = await this.fetchToolchains(localToolchainPath, dependencyToolchainUri) + if (!(toolchainResult instanceof Array)) { + const errorFlavor = toolchainResult === 'CannotReadLocalToolchain' + ? `Could not read Lean version of open project at '${localToolchainPath}'` + : `Could not fetch Lean version of ${dependency.name} at ${dependency.uri}` + const message = `${errorFlavor}. Do you want to update ${dependency.name} without updating the Lean version of the open project to that of ${dependency.name} regardless?` + const input = 'Proceed' + const choice: string | undefined = await window.showInformationMessage(message, { modal: true}, input) + return choice === 'input' ? 'DoNotUpdate' : 'Cancelled' + } + const [localToolchain, dependencyToolchain]: [string, string] = toolchainResult + + if (localToolchain === dependencyToolchain) { + return 'DoNotUpdate' + } + + const message = `The Lean version '${localToolchain}' of the open project differs from the Lean version '${dependencyToolchain}' of ${dependency.name}. Do you want to update the Lean version of the open project to the Lean version of ${dependency.name}?` + const input1 = 'Update Lean Version' + const input2 = 'Keep Lean Version' + const choice = await window.showInformationMessage(message, { modal: true }, input1, input2) + if (choice === undefined) { + return 'Cancelled' + } + if (choice !== input1) { + return 'DoNotUpdate' + } + + return dependencyToolchain + } + + private determineDependencyToolchainUri(dependencyUri: Uri, inputRevision: string): Uri | undefined { + // Example: + // Input: https://github.com/leanprover-community/mathlib4 + // Output: https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain + + if (!dependencyUri.authority.includes('github.com')) { + return undefined + } + const match = dependencyUri.path.match(/\/([^\\]+\/[^\\\.]+)(\.git)?\/?/) + if (!match) { + return undefined + } + const repoPath: string = match[1] + + return Uri.from({ + scheme: 'https', + authority: 'raw.githubusercontent.com', + path: join(repoPath, inputRevision, 'lean-toolchain') + }) + } + + private async fetchToolchains(localToolchainPath: string, dependencyToolchainUri: Uri): Promise<[string, string] | 'CannotReadLocalToolchain' | 'CannotReadDependencyToolchain'> { + let localToolchain: string + try { + localToolchain = fs.readFileSync(localToolchainPath, 'utf8').trim() + } catch (e) { + return 'CannotReadLocalToolchain' + } + + const curlResult: ExecutionResult = await batchExecute('curl', ['-f', '-L', dependencyToolchainUri.toString()]) + if (curlResult.exitCode !== ExecutionExitCode.Success) { + return 'CannotReadDependencyToolchain' + } + const dependencyToolchain: string = curlResult.stdout.trim() + + return [localToolchain, dependencyToolchain] + } + + private async tryFetchingCache(lakeRunner: LakeRunner): Promise<'Success' | 'CacheNotAvailable' | 'Cancelled'> { + const fetchResult: ExecutionResult = await lakeRunner.fetchMathlibCache(true) + switch (fetchResult.exitCode) { + case ExecutionExitCode.Success: + return 'Success' + case ExecutionExitCode.Cancelled: + return 'Cancelled' + default: + return 'CacheNotAvailable' + } + } + + private async runOperation(command: (lakeRunner: LakeRunner) => Promise) { + if (this.isRunningOperation) { + void window.showErrorMessage('Another project action is already being executed. Please wait for its completion.') + return + } + this.isRunningOperation = true + + if (!this.clientProvider) { + void window.showErrorMessage('Lean client has not loaded yet.') + this.isRunningOperation = false + return + } + + const activeClient: LeanClient | undefined = this.clientProvider.getActiveClient() + if (!activeClient) { + void window.showErrorMessage('No active client.') + this.isRunningOperation = false + return + } + + const lakeRunner: LakeRunner = lake(this.channel, activeClient.folderUri) + + const result: 'Success' | 'IsRestarting' = await activeClient.withStoppedClient(() => command(lakeRunner)) + if (result === 'IsRestarting') { + void window.showErrorMessage('Cannot run project action while restarting the server.') + } + + this.isRunningOperation = false + } + + dispose() { + for (const s of this.subscriptions) { s.dispose(); } + } + +} + +interface GitDependencyQuickPickItem extends QuickPickItem, DirectGitDependency { +} diff --git a/vscode-lean4/src/utils/batch.ts b/vscode-lean4/src/utils/batch.ts index 3f962ad76..f1559b653 100644 --- a/vscode-lean4/src/utils/batch.ts +++ b/vscode-lean4/src/utils/batch.ts @@ -1,61 +1,218 @@ -import { OutputChannel } from 'vscode' +import { CancellationToken, Disposable, OutputChannel, ProgressLocation, ProgressOptions, window } from 'vscode' import { spawn } from 'child_process'; import { findProgramInPath, isRunningTest } from '../config' import { logger } from './logger' +import { displayErrorWithOutput } from './errors'; + +export interface ExecutionChannel { + combined?: OutputChannel | undefined + stdout?: OutputChannel | undefined + stderr?: OutputChannel | undefined +} + +export enum ExecutionExitCode { + Success, + CannotLaunch, + ExecutionError, + Cancelled +} + +export interface ExecutionResult { + exitCode: ExecutionExitCode + stdout: string + stderr: string +} + +function createCannotLaunchExecutionResult(message: string): ExecutionResult { + return { + exitCode: ExecutionExitCode.CannotLaunch, + stdout: '', + stderr: message + } +} export async function batchExecute( executablePath: string, - args: any[], - workingDirectory: string | null, - channel: OutputChannel | undefined): Promise { + args: string[], + workingDirectory?: string | undefined, + channel?: ExecutionChannel | undefined, + token?: CancellationToken | undefined): Promise { - return new Promise(function(resolve, reject){ - let output : string = ''; + return new Promise(function(resolve, reject) { + let stdout: string = '' + let stderr: string = '' let options = {} if (workingDirectory !== undefined) { options = { cwd: workingDirectory }; } try { - if (isRunningTest()) - { + if (isRunningTest()) { // The mocha test framework listens to process.on('uncaughtException') // which is raised if spawn cannot find the command and the test automatically // fails with "Uncaught Error: spawn elan ENOENT". Therefore we manually // check if the command exists so as not to trigger that exception. const fullPath = findProgramInPath(executablePath); if (!fullPath) { - resolve(undefined); + resolve(createCannotLaunchExecutionResult('')); return; } } + if (channel?.combined) { + const formattedCwd = workingDirectory ? `${workingDirectory}` : '' + const formattedArgs = args.map(arg => arg.includes(' ') ? `"${arg}"` : arg).join(' ') + channel.combined.appendLine(`${formattedCwd}> ${executablePath} ${formattedArgs}`) + } const proc = spawn(executablePath, args, options); - if (proc.pid === undefined) { - resolve(undefined); - return; - } + const disposeKill: Disposable | undefined = token?.onCancellationRequested(_ => proc.kill()) + + proc.on('error', err => { + disposeKill?.dispose() + resolve(createCannotLaunchExecutionResult(err.message)) + }); proc.stdout.on('data', (line) => { const s: string = line.toString(); - if (channel) channel.appendLine(s); - output += s + '\n'; + if (channel?.combined) channel.combined.appendLine(s) + if (channel?.stdout) channel.stdout.appendLine(s) + stdout += s + '\n'; }); proc.stderr.on('data', (line) => { const s: string = line.toString(); - if (channel) channel.appendLine(s); - output += s + '\n'; + if (channel?.combined) channel.combined.appendLine(s) + if (channel?.stderr) channel.stderr.appendLine(s) + stderr += s + '\n'; }); - proc.on('close', (code) => { + proc.on('close', (code, signal) => { + disposeKill?.dispose() logger.log(`child process exited with code ${code}`); - resolve(output) + if (signal === 'SIGTERM') { + if (channel?.combined) { + channel.combined.appendLine('=> Operation cancelled by user.') + } + resolve({ + exitCode: ExecutionExitCode.Cancelled, + stdout, + stderr + }) + return + } + if (code !== 0) { + if (channel?.combined) { + const formattedCode = code ? `Exit code: ${code}.` : '' + const formattedSignal = signal ? `Signal: ${signal}.` : '' + channel.combined.appendLine(`=> Operation failed. ${formattedCode} ${formattedSignal}`.trim()) + } + resolve({ + exitCode: ExecutionExitCode.ExecutionError, + stdout, + stderr + }) + return + } + resolve({ + exitCode: ExecutionExitCode.Success, + stdout, + stderr + }) }); - } catch (e){ + } catch (e) { logger.log(`error running ${executablePath} : ${e}`); - resolve(undefined); + resolve(createCannotLaunchExecutionResult('')); } }); } + +interface ProgressExecutionOptions { + cwd?: string | undefined + channel?: OutputChannel | undefined + translator?: ((line: string) => string | undefined) | undefined + allowCancellation?: boolean +} + +export async function batchExecuteWithProgress( + executablePath: string, + args: string[], + title: string, + options: ProgressExecutionOptions = {}): Promise { + + const titleSuffix = options.channel ? ' [(Details)](command:lean4.troubleshooting.showOutput)' : '' + + const progressOptions: ProgressOptions = { + location: ProgressLocation.Notification, + title: title + titleSuffix, + cancellable: options.allowCancellation === true + } + let inc = 0 + + const result: ExecutionResult = await window.withProgress(progressOptions, (progress, token) => { + const progressChannel: OutputChannel = { + name : 'ProgressChannel', + append(value: string) { + if (options.translator) { + const translatedValue: string | undefined = options.translator(value) + if (translatedValue === undefined) { + return + } + value = translatedValue + } + if (options.channel) { + options.channel.appendLine(value.trimEnd()) + } + if (inc < 90) { + inc += 2 + } + progress.report({ increment: inc, message: value }) + }, + appendLine(value: string) { + this.append(value + '\n') + }, + replace(_: string) { /* empty */ }, + clear() { /* empty */ }, + show() { /* empty */ }, + hide() { /* empty */ }, + dispose() { /* empty */ } + } + progress.report({ increment: 0 }) + return batchExecute(executablePath, args, options.cwd, { combined: progressChannel }, token); + }); + return result; +} + +type ExecutionHandler = () => Promise + +export interface BatchExecution { + execute: ExecutionHandler + optional?: boolean | undefined // `false` by default +} + +export async function executeAll(executions: BatchExecution[]): Promise { + const results: ExecutionResult[] = [] + for (const execution of executions) { + const result: ExecutionResult = await execution.execute() + results.push(result) + if (execution.optional !== true && result.exitCode !== ExecutionExitCode.Success) { + break + } + } + return results +} + +export async function displayError(result: ExecutionResult, message: string) { + if (result.exitCode === ExecutionExitCode.Success) { + throw Error() + } + const errorMessage: string = formatErrorMessage(result, message) + await displayErrorWithOutput(errorMessage) +} + +function formatErrorMessage(error: ExecutionResult, message: string): string { + if (error.stderr === '') { + return `${message}` + } + return `${message} Command error output: ${error.stderr}` +} diff --git a/vscode-lean4/src/utils/clientProvider.ts b/vscode-lean4/src/utils/clientProvider.ts index b3272aa55..e24f81c14 100644 --- a/vscode-lean4/src/utils/clientProvider.ts +++ b/vscode-lean4/src/utils/clientProvider.ts @@ -1,20 +1,19 @@ -import { Disposable, OutputChannel, workspace, TextDocument, commands, window, EventEmitter, Uri, languages, TextEditor } from 'vscode'; +import { Disposable, OutputChannel, workspace, TextDocument, commands, window, EventEmitter, Uri, languages, TextEditor, WorkspaceFolder } from 'vscode'; import { LeanInstaller, LeanVersion } from './leanInstaller' import { LeanpkgService } from './leanpkg'; import { LeanClient } from '../leanclient' import { LeanFileProgressProcessingInfo, ServerStoppedReason } from '@leanprover/infoview-api'; import * as path from 'path'; -import { findLeanPackageRoot } from './projectInfo'; +import { checkParentFoldersForLeanProject, findLeanPackageRoot, isValidLeanProject } from './projectInfo'; import { isFileInFolder } from './fsHelper'; import { logger } from './logger' -import { addDefaultElanPath, getDefaultElanPath, addToolchainBinPath, isElanDisabled, isRunningTest } from '../config' +import { addDefaultElanPath, getDefaultElanPath, addToolchainBinPath, isElanDisabled, isRunningTest, shouldShowInvalidProjectWarnings } from '../config' // This class ensures we have one LeanClient per workspace folder. export class LeanClientProvider implements Disposable { private subscriptions: Disposable[] = []; private outputChannel: OutputChannel; private installer : LeanInstaller; - private pkgService : LeanpkgService; private versions: Map = new Map(); private clients: Map = new Map(); private pending: Map = new Map(); @@ -34,18 +33,17 @@ export class LeanClientProvider implements Disposable { private clientStoppedEmitter = new EventEmitter<[LeanClient, boolean, ServerStoppedReason]>() clientStopped = this.clientStoppedEmitter.event - constructor(installer : LeanInstaller, pkgService : LeanpkgService, outputChannel : OutputChannel) { + constructor(installer: LeanInstaller, outputChannel: OutputChannel) { this.outputChannel = outputChannel; this.installer = installer; - this.pkgService = pkgService; // we must setup the installChanged event handler first before any didOpenEditor calls. installer.installChanged(async (uri: Uri) => await this.onInstallChanged(uri)); // Only change the document language for *visible* documents, // because this closes and then reopens the document. - window.visibleTextEditors.forEach((e) => this.didOpenEditor(e.document)); - this.subscriptions.push(window.onDidChangeVisibleTextEditors((es) => - es.forEach((e) => this.didOpenEditor(e.document)))); + window.visibleTextEditors.forEach(e => this.didOpenEditor(e.document)); + this.subscriptions.push(window.onDidChangeVisibleTextEditors(es => + es.forEach(e => this.didOpenEditor(e.document)))); this.subscriptions.push( commands.registerCommand('lean4.restartFile', () => this.restartFile()), @@ -54,7 +52,7 @@ export class LeanClientProvider implements Disposable { commands.registerCommand('lean4.stopServer', () => this.stopActiveClient()) ); - workspace.onDidOpenTextDocument((document) => this.didOpenEditor(document)); + workspace.onDidOpenTextDocument(document => this.didOpenEditor(document)); workspace.onDidChangeWorkspaceFolders((event) => { for (const folder of event.removed) { @@ -89,10 +87,10 @@ export class LeanClientProvider implements Disposable { { try { const uri = this.pendingInstallChanged.pop(); - if (uri){ + if (uri) { // have to check again here in case elan install had --default-toolchain none. const [workspaceFolder, folder, packageFileUri] = await findLeanPackageRoot(uri); - const packageUri = folder ? folder : Uri.from({scheme: 'untitled'}); + const packageUri = folder ?? Uri.from({scheme: 'untitled'}); logger.log('[ClientProvider] testLeanVersion'); const version = await this.installer.testLeanVersion(packageUri); if (version.version === '4') { @@ -115,14 +113,16 @@ export class LeanClientProvider implements Disposable { private async autoInstall() : Promise { // no prompt, just do it! - const version = this.installer.getDefaultToolchain(); - logger.log(`[ClientProvider] Installing ${version} via Elan during testing`); await this.installer.installElan(); if (isElanDisabled()) { addToolchainBinPath(getDefaultElanPath()); } else { addDefaultElanPath(); } + + for (const [_, client] of this.clients) { + await this.onInstallChanged(client.folderUri) + } } private getVisibleEditor(uri: Uri) : TextEditor | null { @@ -136,17 +136,33 @@ export class LeanClientProvider implements Disposable { } private restartFile() { - if (window.activeTextEditor && this.activeClient && window.activeTextEditor.document.languageId ==='lean4') { - void this.activeClient.restartFile(window.activeTextEditor.document); + if (!this.activeClient || !this.activeClient.isRunning()) { + void window.showErrorMessage('No active client.') + return + } + + if (!window.activeTextEditor || window.activeTextEditor.document.languageId !== 'lean4') { + void window.showErrorMessage('No active Lean editor tab. Make sure to focus the Lean editor tab for which you want to issue a restart.') + return } + + void this.activeClient.restartFile(window.activeTextEditor.document); } private stopActiveClient() { - void this.activeClient?.stop(); + if (this.activeClient && this.activeClient.isStarted()) { + void this.activeClient?.stop(); + } } - private restartActiveClient() { - void this.activeClient?.restart(); + private async restartActiveClient() { + const result: string | undefined = await window.showInformationMessage( + 'Restart Lean 4 server to re-elaborate all open files?', + { modal: true }, + 'Restart server') + if (result === 'Restart server') { + void this.activeClient?.restart(); + } } clientIsStarted() { @@ -154,8 +170,6 @@ export class LeanClientProvider implements Disposable { } async didOpenEditor(document: TextDocument) { - this.pkgService.didOpen(document.uri); - // bail as quickly as possible on non-lean files. if (document.languageId !== 'lean' && document.languageId !== 'lean4') { return; @@ -186,9 +200,13 @@ export class LeanClientProvider implements Disposable { try { const [cached, client] = await this.ensureClient(document.uri, undefined); - if (client) { - await client.openLean4Document(document) + if (!client) { + return } + + await this.checkIsValidProjectFolder(client.folderUri) + + await client.openLean4Document(document) } catch (e) { logger.log(`[ClientProvider] ### Error opening document: ${e}`); } @@ -223,7 +241,7 @@ export class LeanClientProvider implements Disposable { } getClientForFolder(folder: Uri) : LeanClient | undefined { - let client: LeanClient | undefined; + let client: LeanClient | undefined; const key = this.getKeyFromUri(folder); const cachedClient = this.clients.has(key); if (cachedClient) { @@ -275,7 +293,7 @@ export class LeanClientProvider implements Disposable { // Returns a null client if it turns out the new workspace is a lean3 workspace. async ensureClient(uri : Uri, versionInfo: LeanVersion | undefined) : Promise<[boolean,LeanClient | undefined]> { const [workspaceFolder, folder, packageFileUri] = await findLeanPackageRoot(uri); - const folderUri = folder ? folder : Uri.from({scheme: 'untitled'}); + const folderUri = folder ?? Uri.from({scheme: 'untitled'}); let client = this.getClientForFolder(folderUri); const key = this.getKeyFromUri(folder); const cachedClient = (client !== undefined); @@ -356,6 +374,37 @@ export class LeanClientProvider implements Disposable { return [cachedClient, client]; } + private async checkIsValidProjectFolder(folderUri: Uri) { + if (!shouldShowInvalidProjectWarnings()) { + return + } + + if (folderUri.scheme !== 'file') { + void window.showWarningMessage('Lean 4 server operating in restricted single file mode. Please open a valid Lean 4 project containing a \'lean-toolchain\' file for full functionality.') + return + } + + if (await isValidLeanProject(folderUri)) { + return + } + + const parentProjectFolder: Uri | undefined = await checkParentFoldersForLeanProject(folderUri) + if (parentProjectFolder === undefined) { + void window.showWarningMessage('Opened folder is not a valid Lean 4 project. Please open a valid Lean 4 project containing a \'lean-toolchain\' file for full functionality.') + return + } + + const message = `Opened folder is not a valid Lean 4 project folder because it does not contain a 'lean-toolchain' file. +However, a valid Lean 4 project folder was found in one of the parent directories at '${parentProjectFolder.fsPath}'. +Open this project instead?` + const input = 'Open parent directory project' + const choice: string | undefined = await window.showWarningMessage(message, input) + if (choice === input) { + // this kills the extension host + await commands.executeCommand('vscode.openFolder', parentProjectFolder) + } + } + dispose(): void { for (const s of this.subscriptions) { s.dispose(); } } diff --git a/vscode-lean4/src/utils/elan.ts b/vscode-lean4/src/utils/elan.ts new file mode 100644 index 000000000..d707686c1 --- /dev/null +++ b/vscode-lean4/src/utils/elan.ts @@ -0,0 +1,6 @@ +import { OutputChannel } from 'vscode'; +import { ExecutionResult, batchExecuteWithProgress } from './batch'; + +export async function elanSelfUpdate(channel: OutputChannel): Promise { + return await batchExecuteWithProgress('elan', ['self', 'update'], 'Updating Elan', { channel }) +} diff --git a/vscode-lean4/src/utils/errors.ts b/vscode-lean4/src/utils/errors.ts new file mode 100644 index 000000000..5910c4619 --- /dev/null +++ b/vscode-lean4/src/utils/errors.ts @@ -0,0 +1,9 @@ +import { commands, window } from 'vscode'; + +export async function displayErrorWithOutput(message: string) { + const input = 'Show Output' + const choice = await window.showErrorMessage(message, input) + if (choice === input) { + await commands.executeCommand('lean4.troubleshooting.showOutput') + } +} diff --git a/vscode-lean4/src/utils/lake.ts b/vscode-lean4/src/utils/lake.ts new file mode 100644 index 000000000..bc7b91c53 --- /dev/null +++ b/vscode-lean4/src/utils/lake.ts @@ -0,0 +1,90 @@ +import { OutputChannel, Uri } from 'vscode'; +import { ExecutionExitCode, ExecutionResult, batchExecute, batchExecuteWithProgress } from './batch'; + +export const cacheNotFoundError = 'unknown executable `cache`' +export const cacheNotFoundExitError = '=> Operation failed. Exit Code: 1.' + +export class LakeRunner { + channel: OutputChannel + cwdUri: Uri | undefined + toolchain: string | undefined + + constructor(channel: OutputChannel, cwdUri: Uri | undefined, toolchain?: string | undefined) { + this.channel = channel + this.cwdUri = cwdUri + this.toolchain = toolchain + } + + async initProject(name: string, kind?: string | undefined): Promise { + const args = kind ? [name, kind] : [name] + return this.runLakeCommandWithProgress('init', args, 'Initializing project') + } + + async updateDependencies(): Promise { + return this.runLakeCommandWithProgress('update', [], 'Updating dependencies') + } + + async updateDependency(dependencyName: string): Promise { + return this.runLakeCommandWithProgress('update', [dependencyName], `Updating '${dependencyName}' dependency`) + } + + async build(): Promise { + return this.runLakeCommandWithProgress('build', [], 'Building Lean project') + } + + async clean(): Promise { + return this.runLakeCommandWithProgress('clean', [], 'Cleaning Lean project') + } + + async fetchMathlibCache(filterError: boolean = false): Promise { + const prompt = 'Checking Mathlib build artifact cache' + return this.runLakeCommandWithProgress('exe', ['cache', 'get'], prompt, line => { + if (filterError && line.includes(cacheNotFoundError)) { + return undefined + } + return line + }) + } + + async isMathlibCacheGetAvailable(): Promise<'Yes' | 'No' | 'Cancelled'> { + const result: ExecutionResult = await this.runLakeCommandWithProgress('exe', ['cache'], 'Checking whether this is a Mathlib project') + if (result.exitCode === ExecutionExitCode.Cancelled) { + return 'Cancelled' + } + if (result.exitCode === ExecutionExitCode.Success) { + return 'Yes' + } + return 'No' + } + + private async runLakeCommandSilently(subCommand: string, args: string[]): Promise { + args = args.slice() + args.unshift(subCommand) + if (this.toolchain) { + args.unshift(`+${this.toolchain}`) + } + return await batchExecute('lake', args, this.cwdUri?.fsPath) + } + + private async runLakeCommandWithProgress( + subCommand: string, + args: string[], + waitingPrompt: string, + translator?: ((line: string) => string | undefined) | undefined): Promise { + args = args.slice() + args.unshift(subCommand) + if (this.toolchain) { + args.unshift(`+${this.toolchain}`) + } + return await batchExecuteWithProgress('lake', args, waitingPrompt, { + cwd: this.cwdUri?.fsPath, + channel: this.channel, + translator, + allowCancellation: true + }) + } +} + +export function lake(channel: OutputChannel, cwdUri: Uri | undefined, toolchain?: string | undefined): LakeRunner { + return new LakeRunner(channel, cwdUri, toolchain) +} diff --git a/vscode-lean4/src/utils/leanInstaller.ts b/vscode-lean4/src/utils/leanInstaller.ts index e851832d8..b052105ae 100644 --- a/vscode-lean4/src/utils/leanInstaller.ts +++ b/vscode-lean4/src/utils/leanInstaller.ts @@ -1,6 +1,6 @@ import { window, TerminalOptions, OutputChannel, Disposable, EventEmitter, ProgressLocation, Uri } from 'vscode' import { toolchainPath, addServerEnvPaths, getPowerShellPath, shouldAutofocusOutput, isRunningTest } from '../config' -import { batchExecute } from './batch' +import { ExecutionExitCode, ExecutionResult, batchExecute, batchExecuteWithProgress } from './batch' import { readLeanVersion, isCoreLean4Directory } from './projectInfo'; import { join } from 'path'; import { logger } from './logger' @@ -10,12 +10,11 @@ export class LeanVersion { error: string | undefined; } -export class LeanInstaller implements Disposable { +export class LeanInstaller { private leanInstallerLinux = 'https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh' private leanInstallerWindows = 'https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1' private outputChannel: OutputChannel; - private subscriptions: Disposable[] = []; private prompting : boolean = false; private defaultToolchain : string; // the default to use if there is no elan installed private elanDefaultToolchain : string = ''; // the default toolchain according to elan (toolchain marked with '(default)') @@ -44,6 +43,10 @@ export class LeanInstaller implements Disposable { return this.promptUser; } + getOutputChannel(): OutputChannel { + return this.outputChannel + } + async testLeanVersion(packageUri: Uri) : Promise { // see if there is a lean-toolchain file and use that version info. @@ -82,23 +85,25 @@ export class LeanInstaller implements Disposable { } async handleVersionChanged(packageUri : Uri) : Promise { - if (packageUri && packageUri.scheme === 'file'){ + if (packageUri && packageUri.scheme === 'file') { const key = packageUri.fsPath; if (this.versionCache.has(key)) { this.versionCache.delete(key); } } - if (this.promptUser){ - if (this.prompting) { - return; - } - const restartItem = 'Restart Lean'; - const item = await this.showPrompt('Lean version changed', restartItem); - if (item === restartItem) { - await this.checkAndFire(packageUri); - } - } else { + if (!this.promptUser) { + await this.checkAndFire(packageUri); + return + } + + if (this.prompting) { + return; + } + + const restartItem = 'Restart Lean'; + const item = await this.showPrompt('Lean version changed', restartItem); + if (item === restartItem) { await this.checkAndFire(packageUri); } } @@ -123,16 +128,18 @@ export class LeanInstaller implements Disposable { } async handleLakeFileChanged(uri: Uri) : Promise { - if (this.promptUser){ - if (this.prompting) { - return; - } - const restartItem = 'Restart Lean'; - const item = await this.showPrompt('Lake file configuration changed', restartItem); - if (item === restartItem) { - this.installChangedEmitter.fire(uri); - } - } else { + if (!this.promptUser) { + this.installChangedEmitter.fire(uri); + return + } + + if (this.prompting) { + return; + } + + const restartItem = 'Restart Lean'; + const item = await this.showPrompt('Lake file configuration changed', restartItem); + if (item === restartItem) { this.installChangedEmitter.fire(uri); } } @@ -159,7 +166,7 @@ export class LeanInstaller implements Disposable { const item = await this.showPrompt(prompt, installItem) if (item === installItem) { try { - const result = await this.installElan(); + await this.installElan(); this.installChangedEmitter.fire(uri); } catch (err) { const msg = '' + err; @@ -206,7 +213,7 @@ export class LeanInstaller implements Disposable { } } - const env = addServerEnvPaths(process.env); + addServerEnvPaths(process.env); let options = ['--version'] if (version) { @@ -221,18 +228,16 @@ export class LeanInstaller implements Disposable { // looks for a global (default) installation of Lean. This way, we can support // single file editing. logger.log(`executeWithProgress ${cmd} ${options}`) - const stdout = await this.executeWithProgress('Checking Lean setup...', cmd, options, folderPath) - if (!stdout) { + const checkingResult: ExecutionResult = await batchExecute(cmd, options, folderPath, { combined: this.outputChannel }) + if (checkingResult.exitCode === ExecutionExitCode.CannotLaunch) { result.error = 'lean not found' - } - else if (stdout.indexOf('no default toolchain') > 0) { + } else if (checkingResult.stderr.indexOf('no default toolchain') > 0) { result.error = 'no default toolchain' - } - else { + } else { const filterVersion = /version (\d+)\.\d+\..+/ - const match = filterVersion.exec(stdout) + const match = filterVersion.exec(checkingResult.stdout) if (!match) { - return { version: '', error: `lean4: '${cmd} ${options}' returned incorrect version string '${stdout}'.` } + return { version: '', error: `lean4: '${cmd} ${options}' returned incorrect version string '${checkingResult.stdout}'.` } } const major = match[1]; result.version = major @@ -247,47 +252,6 @@ export class LeanInstaller implements Disposable { return result } - private async executeWithProgress(prompt: string, cmd: string, options: string[], workingDirectory: string | null): Promise{ - let inc = 0; - let stdout = '' - /* eslint-disable @typescript-eslint/no-this-alias */ - const realThis = this; - await window.withProgress({ - location: ProgressLocation.Notification, - title: '', - cancellable: false - }, (progress) => { - const progressChannel : OutputChannel = { - name : 'ProgressChannel', - append(value: string) - { - stdout += value; - if (realThis.outputChannel){ - // add the output here in case user wants to go look for it. - const msg = value.trim(); - logger.log(`[LeanInstaller] ${cmd} returned: ${msg}`); - realThis.outputChannel.appendLine(msg); - } - if (inc < 100) { - inc += 10; - } - progress.report({ increment: inc, message: value }); - }, - appendLine(value: string) { - this.append(value + '\n'); - }, - replace(value: string) { /* empty */ }, - clear() { /* empty */ }, - show() { /* empty */ }, - hide() { /* empty */ }, - dispose() { /* empty */ } - } - progress.report({increment:0, message: prompt}); - return batchExecute(cmd, options, workingDirectory, progressChannel); - }); - return stdout; - } - getDefaultToolchain() : string { return this.defaultToolchain; } @@ -319,7 +283,7 @@ export class LeanInstaller implements Disposable { try { const cmd = 'elan'; const options = ['toolchain', 'list']; - const stdout = await batchExecute(cmd, options, folderPath, undefined); + const stdout = (await batchExecute(cmd, options, folderPath)).stdout if (!stdout){ throw new Error('elan toolchain list returned no output.'); } @@ -337,77 +301,66 @@ export class LeanInstaller implements Disposable { } async hasElan() : Promise { - let elanInstalled = false; - // See if we have elan already. try { const options = ['--version'] - const stdout = await this.executeWithProgress('Checking Elan setup...', 'elan', options, null) + const result = await batchExecute('elan', options) const filterVersion = /elan (\d+)\.\d+\..+/ - const match = filterVersion.exec(stdout) - if (match) { - elanInstalled = true; - } + const match = filterVersion.exec(result.stdout) + return match !== null } catch (err) { - elanInstalled = false; + return false } - return elanInstalled; } async installElan() : Promise { - if (toolchainPath()) { void window.showErrorMessage('It looks like you\'ve modified the `lean.toolchainPath` user setting.' + 'Please clear this setting before installing elan.'); return false; - } else { - const terminalName = 'Lean installation via elan'; - - let terminalOptions: TerminalOptions = { name: terminalName }; - if (process.platform === 'win32') { - terminalOptions = { name: terminalName, shellPath: getPowerShellPath() }; - } - const terminal = window.createTerminal(terminalOptions); - terminal.show(); - - // We register a listener, to restart the Lean extension once elan has finished. - const result = new Promise(function(resolve, reject) { - window.onDidCloseTerminal(async (t) => { - if (t === terminal) { - resolve(true); - } else { - logger.log('[LeanInstaller] ignoring terminal closed: ' + t.name + ', waiting for: ' + terminalName); - }}); - }); + } - if (process.platform === 'win32') { - terminal.sendText( - `Start-BitsTransfer -Source "${this.leanInstallerWindows}" -Destination "elan-init.ps1"\r\n` + - 'Set-ExecutionPolicy -ExecutionPolicy Unrestricted -Scope Process\r\n' + - `$rc = .\\elan-init.ps1 -NoPrompt 1 -DefaultToolchain ${this.defaultToolchain}\r\n` + - 'Write-Host "elan-init returned [$rc]"\r\n' + - 'del .\\elan-init.ps1\r\n' + - 'if ($rc -ne 0) {\r\n' + - ' Read-Host -Prompt "Press ENTER to continue"\r\n' + - '}\r\n' + - 'exit\r\n' - ); - } - else { - const elanArgs = `-y --default-toolchain ${this.defaultToolchain}`; - const prompt = '(echo && read -n 1 -s -r -p "Install failed, press ENTER to continue...")'; + const terminalName = 'Lean installation via elan'; - terminal.sendText(`bash -c 'curl ${this.leanInstallerLinux} -sSf | sh -s -- ${elanArgs} || ${prompt}' && exit `); - } + let terminalOptions: TerminalOptions = { name: terminalName }; + if (process.platform === 'win32') { + terminalOptions = { name: terminalName, shellPath: getPowerShellPath() }; + } + const terminal = window.createTerminal(terminalOptions); + terminal.show(); + + // We register a listener, to restart the Lean extension once elan has finished. + const result = new Promise(function(resolve, reject) { + window.onDidCloseTerminal(async (t) => { + if (t === terminal) { + resolve(true); + } else { + logger.log('[LeanInstaller] ignoring terminal closed: ' + t.name + ', waiting for: ' + terminalName); + }}); + }); - // clear any previous lean version errors. - this.versionCache.clear(); - this.elanDefaultToolchain = this.defaultToolchain; + if (process.platform === 'win32') { + terminal.sendText( + `Start-BitsTransfer -Source "${this.leanInstallerWindows}" -Destination "elan-init.ps1"\r\n` + + 'Set-ExecutionPolicy -ExecutionPolicy Unrestricted -Scope Process\r\n' + + `$rc = .\\elan-init.ps1 -NoPrompt 1 -DefaultToolchain ${this.defaultToolchain}\r\n` + + 'Write-Host "elan-init returned [$rc]"\r\n' + + 'del .\\elan-init.ps1\r\n' + + 'if ($rc -ne 0) {\r\n' + + ' Read-Host -Prompt "Press ENTER to continue"\r\n' + + '}\r\n' + + 'exit\r\n' + ); + } else { + const elanArgs = `-y --default-toolchain ${this.defaultToolchain}`; + const prompt = '(echo && read -n 1 -s -r -p "Install failed, press ENTER to continue...")'; - return result; + terminal.sendText(`bash -c 'curl ${this.leanInstallerLinux} -sSf | sh -s -- ${elanArgs} || ${prompt}' && exit `); } - } - dispose(): void { - for (const s of this.subscriptions) { s.dispose(); } + // clear any previous lean version errors. + this.versionCache.clear(); + this.elanDefaultToolchain = this.defaultToolchain; + + return result; } } diff --git a/vscode-lean4/src/utils/leanpkg.ts b/vscode-lean4/src/utils/leanpkg.ts index 3f4020654..91c10ee1c 100644 --- a/vscode-lean4/src/utils/leanpkg.ts +++ b/vscode-lean4/src/utils/leanpkg.ts @@ -24,7 +24,6 @@ export class LeanpkgService implements Disposable { lakeFileChanged = this.lakeFileChangedEmitter.event constructor() { - // track changes in the version of lean specified in the lean-toolchain file // or the leanpkg.toml. While this is looking for all files with these names // it ignores files that are not in the package root. @@ -41,6 +40,11 @@ export class LeanpkgService implements Disposable { watcher2.onDidDelete((u) => this.handleLakeFileChanged(u, true)); this.subscriptions.push(watcher); }); + + window.visibleTextEditors.forEach(e => this.didOpen(e.document.uri)); + this.subscriptions.push(window.onDidChangeVisibleTextEditors(es => + es.forEach(e => this.didOpen(e.document.uri)))); + workspace.onDidOpenTextDocument(document => this.didOpen(document.uri)); } dispose(): void { @@ -49,7 +53,7 @@ export class LeanpkgService implements Disposable { // Must be called when every file is opened so it can track the current contents // of the files we care about. - didOpen(uri: Uri){ + private didOpen(uri: Uri){ const fileName = path.basename(uri.fsPath); if (fileName === this.lakeFileName){ void this.handleLakeFileChanged(uri, false); @@ -66,51 +70,61 @@ export class LeanpkgService implements Disposable { // Note: just opening the file fires this event sometimes which is annoying, so // we compare the contents just to be sure and normalize whitespace so that // just adding a new line doesn't trigger the prompt. - const [workspaceFolder, packageUri, packageFileUri] = await findLeanPackageRoot(uri); - if (packageUri) { - const fileUri = await this.findLakeFile(packageUri); - if (fileUri) { - const contents = await this.readWhitespaceNormalized(fileUri); - let existing : string | undefined; - const key = packageUri.toString(); - if (this.normalizedLakeFileContents.get(key)){ - existing = this.normalizedLakeFileContents.get(key); - } - if (contents !== existing) { - this.normalizedLakeFileContents.set(key, contents); - if (raiseEvent) { - // raise an event so the extension triggers handleLakeFileChanged. - this.lakeFileChangedEmitter.fire(packageUri); - } - } - } + const [_1, packageUri, _2] = await findLeanPackageRoot(uri) + if (!packageUri) { + return + } + + const fileUri = await this.findLakeFile(packageUri) + if (!fileUri) { + return + } + + const contents = await this.readWhitespaceNormalized(fileUri) + let existing : string | undefined + const key = packageUri.toString() + if (this.normalizedLakeFileContents.get(key)) { + existing = this.normalizedLakeFileContents.get(key) + } + if (contents === existing) { + return + } + + this.normalizedLakeFileContents.set(key, contents) + if (raiseEvent) { + // raise an event so the extension triggers handleLakeFileChanged. + this.lakeFileChangedEmitter.fire(packageUri) } } private async handleFileChanged(uri: Uri, raiseEvent : boolean) { // note: apply the same rules here with findLeanPkgVersionInfo no matter // if a file is added or removed so we always match the elan behavior. - const [packageUri, version] = await findLeanPackageVersionInfo(uri); - if (packageUri && version) { - let existing : string | undefined; - const key = packageUri.toString(); - if (this.currentVersion.has(key)){ - existing = this.currentVersion.get(key); - } - if (existing !== version){ - this.currentVersion.set(key, version); - if (raiseEvent) { - // raise an event so the extension triggers handleVersionChanged. - this.versionChangedEmitter.fire(packageUri); - } - } + const [packageUri, version] = await findLeanPackageVersionInfo(uri) + if (!packageUri || !version) { + return + } + + let existing: string | undefined + const key = packageUri.toString() + if (this.currentVersion.has(key)){ + existing = this.currentVersion.get(key) + } + if (existing === version) { + return + } + + this.currentVersion.set(key, version) + if (raiseEvent) { + // raise an event so the extension triggers handleVersionChanged. + this.versionChangedEmitter.fire(packageUri) } } private async findLakeFile(packageUri: Uri) : Promise { const fullPath = Uri.joinPath(packageUri, this.lakeFileName); const url = fullPath.fsPath; - if(await fileExists(url)) { + if (await fileExists(url)) { return fullPath; } return null; diff --git a/vscode-lean4/src/utils/manifest.ts b/vscode-lean4/src/utils/manifest.ts new file mode 100644 index 000000000..81fb1af46 --- /dev/null +++ b/vscode-lean4/src/utils/manifest.ts @@ -0,0 +1,89 @@ +import { join } from 'path' +import { Uri } from 'vscode' +import { z } from 'zod' +import * as fs from 'fs' + +export interface DirectGitDependency { + name: string + uri: Uri + revision: string + inputRevision: string +} + +export interface Manifest { + directGitDependencies: DirectGitDependency[] +} + +export function parseAsManifest(jsonString: string): Manifest | undefined { + let parsedJson: any + try { + parsedJson = JSON.parse(jsonString) + } catch (e) { + return undefined + } + + const schema = z.object({ + packages: z.array( + z.union([ + z.object({ + git: z.object({ + name: z.string(), + url: z.string().url(), + rev: z.string(), + inherited: z.boolean(), + 'inputRev?': z.optional(z.nullable(z.string())) + }) + }), + z.object({ + path: z.any() + }) + ]) + ) + }) + const result = schema.safeParse(parsedJson) + if (!result.success) { + return undefined + } + + const manifest: Manifest = { directGitDependencies: [] } + + for (const pkg of result.data.packages) { + if (!('git' in pkg)) { + continue + } + if (pkg.git.inherited) { + continue // Inherited Git packages are not direct dependencies + } + + const inputRev: string | null | undefined = pkg.git['inputRev?'] + + manifest.directGitDependencies.push({ + name: pkg.git.name, + uri: Uri.parse(pkg.git.url), + revision: pkg.git.rev, + inputRevision: inputRev ? inputRev : 'master' // Lake also always falls back to master + }) + } + + return manifest +} + +export type ManifestReadError = string + +export async function parseManifestInFolder(folderUri: Uri): Promise { + const manifestPath: string = join(folderUri.fsPath, 'lake-manifest.json') + + let jsonString: string + try { + jsonString = fs.readFileSync(manifestPath, 'utf8') + } catch (e) { + return `Cannot read 'lake-manifest.json' file at ${manifestPath} to determine dependencies.` + } + + const manifest: Manifest | undefined = parseAsManifest(jsonString) + if (!manifest) { + return `Cannot parse 'lake-manifest.json' file at ${manifestPath} to determine dependencies.` + } + + return manifest +} diff --git a/vscode-lean4/src/utils/projectInfo.ts b/vscode-lean4/src/utils/projectInfo.ts index c8102ef7d..91ae23b74 100644 --- a/vscode-lean4/src/utils/projectInfo.ts +++ b/vscode-lean4/src/utils/projectInfo.ts @@ -1,29 +1,33 @@ import * as fs from 'fs'; import { URL } from 'url'; -import { Uri, workspace, WorkspaceFolder } from 'vscode'; +import { FileType, Uri, workspace, WorkspaceFolder } from 'vscode'; import { fileExists } from './fsHelper'; import { logger } from './logger' +import path = require('path'); // Detect lean4 root directory (works for both lean4 repo and nightly distribution) export async function isCoreLean4Directory(path: Uri): Promise { - if (path.scheme === 'file'){ - return await fileExists(Uri.joinPath(path, 'LICENSE').fsPath) && await fileExists(Uri.joinPath(path, 'LICENSES').fsPath); + if (path.scheme !== 'file') { + return false } - return false; + + const licensePath = Uri.joinPath(path, 'LICENSE').fsPath + const licensesPath = Uri.joinPath(path, 'LICENSES').fsPath + const srcPath = Uri.joinPath(path, 'src').fsPath + return await fileExists(licensePath) + && await fileExists(licensesPath) + && await fileExists(srcPath) } // Find the root of a Lean project and return an optional WorkspaceFolder for it, // the Uri for the package root and the Uri for the 'leanpkg.toml' or 'lean-toolchain' file found there. export async function findLeanPackageRoot(uri: Uri) : Promise<[WorkspaceFolder | undefined, Uri | null, Uri | null]> { - if (!uri) return [undefined, null, null]; + if (!uri || uri.scheme !== 'file') return [undefined, null, null]; const toolchainFileName = 'lean-toolchain'; const tomlFileName = 'leanpkg.toml'; - if (uri.scheme === 'untitled'){ - // then return a Uri representing all untitled files. - return [undefined, Uri.from({scheme: 'untitled'}), null]; - } + let path = uri; let wsFolder = workspace.getWorkspaceFolder(uri); if (!wsFolder && workspace.workspaceFolders) { @@ -37,7 +41,7 @@ export async function findLeanPackageRoot(uri: Uri) : Promise<[WorkspaceFolder | if (wsFolder){ // jump to the real workspace folder if we have a Workspace for this file. path = wsFolder.uri; - } else if (path.scheme === 'file') { + } else { // then start searching from the directory containing this document. // The given uri may already be a folder Uri in some cases. if (fs.lstatSync(path.fsPath).isFile()) { @@ -47,34 +51,28 @@ export async function findLeanPackageRoot(uri: Uri) : Promise<[WorkspaceFolder | } const startFolder = path; - if (path.scheme === 'file') { - // search parent folders for a leanpkg.toml file, or a Lake lean-toolchain file. - while (true) { - // give preference to 'lean-toolchain' files if any. - const leanToolchain = Uri.joinPath(path, toolchainFileName); - if (await fileExists(leanToolchain.fsPath)) { - return [wsFolder, path, leanToolchain]; - } - else { - const leanPkg = Uri.joinPath(path, tomlFileName); - if (await fileExists(leanPkg.fsPath)) { - return [wsFolder, path, leanPkg]; - } - else if (await isCoreLean4Directory(path)) { - return [wsFolder, path, null]; - } - else if (searchUpwards) { - const parent = Uri.joinPath(path, '..'); - if (parent === path) { - // no project file found. - break; - } - path = parent; - } - else { - // don't search above a WorkspaceFolder barrier. + // search parent folders for a leanpkg.toml file, or a Lake lean-toolchain file. + while (true) { + // give preference to 'lean-toolchain' files if any. + const leanToolchain = Uri.joinPath(path, toolchainFileName); + if (await fileExists(leanToolchain.fsPath)) { + return [wsFolder, path, leanToolchain]; + } else { + const leanPkg = Uri.joinPath(path, tomlFileName); + if (await fileExists(leanPkg.fsPath)) { + return [wsFolder, path, leanPkg]; + } else if (await isCoreLean4Directory(path)) { + return [wsFolder, path, null]; + } else if (searchUpwards) { + const parent = Uri.joinPath(path, '..'); + if (parent === path) { + // no project file found. break; } + path = parent; + } else { + // don't search above a WorkspaceFolder barrier. + break; } } } @@ -88,7 +86,7 @@ export async function findLeanPackageRoot(uri: Uri) : Promise<[WorkspaceFolder | export async function findLeanPackageVersionInfo(uri: Uri) : Promise<[Uri | null, string | null]> { const [_, packageUri, packageFileUri] = await findLeanPackageRoot(uri); - if (!packageUri || packageUri.scheme === 'untitled') return [null, null]; + if (!packageUri) return [null, null]; let version : string | null = null; if (packageFileUri) { @@ -144,3 +142,27 @@ async function readLeanVersionFile(packageFileUri : Uri) : Promise { return ''; } + +export async function isValidLeanProject(projectFolder: Uri): Promise { + try { + const leanToolchainPath = Uri.joinPath(projectFolder, 'lean-toolchain').fsPath + + const isLeanProject: boolean = await fileExists(leanToolchainPath) + const isLeanItself: boolean = await isCoreLean4Directory(projectFolder) + return isLeanProject || isLeanItself + } catch { + return false + } +} + +export async function checkParentFoldersForLeanProject(folder: Uri): Promise { + let childFolder: Uri + do { + childFolder = folder + folder = Uri.file(path.dirname(folder.fsPath)) + if (await isValidLeanProject(folder)) { + return folder + } + } while (childFolder.fsPath !== folder.fsPath) + return undefined +}