Add project commands, command menu and walkthrough (#334)

.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

.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
+    }
 }

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

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.

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.

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.

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.

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.

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.

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.

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).