diff --git a/doc/images/code-ext.png b/doc/images/code-ext.png new file mode 100644 index 0000000000..9921ea05b6 Binary files /dev/null and b/doc/images/code-ext.png differ diff --git a/doc/images/code-success.png b/doc/images/code-success.png new file mode 100644 index 0000000000..9aaa7b908b Binary files /dev/null and b/doc/images/code-success.png differ diff --git a/doc/quickstart.md b/doc/quickstart.md new file mode 100644 index 0000000000..899f22fdb8 --- /dev/null +++ b/doc/quickstart.md @@ -0,0 +1,22 @@ +# Quickstart + +These instructions will walk you through setting up Lean using the "basic" setup and VS Code as the editor. +See [Setup](./setup.md) for other ways and more details on setting up Lean. + +1. Install the latest Lean 4 nightly through [`elan`](https://github.com/Kha/elan): in any bash-compatible shell, run +```sh +$ curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain leanprover/lean4:nightly +``` +See the `elan` link above for other installation options and details. +1. Install [VS Code](https://code.visualstudio.com/). +1. Open VS Code and install the `lean4` extension. ![installing the vscode-lean4 extension](images/code-ext.png) +1. Create a new file with the extension `.lean` and add the following code: +```lean +import Leanpkg + +#eval Leanpkg.leanVersionString +``` +You should get a syntax-highlighted file with an "infoview" on the right that tells you the installed Lean version when placing your cursor on the last line. ![successful setup](images/code-success.png) +1. You are set up! Try opening a Lean package with a `leanpkg.toml`. You can create your own packages using `leanpkg init` on the command line. +Packages **have** to be opened using "File > Open Folder..." for imports to work. +Saved changes are visibly in other files after running "Lean 4: Refresh File Dependencies" (`Ctrl+Shift+X`) in them. diff --git a/doc/setup.md b/doc/setup.md index 400e975d6f..e719fc83ac 100644 --- a/doc/setup.md +++ b/doc/setup.md @@ -5,6 +5,8 @@ There are currently two ways to set up a Lean 4 development environment: * [basic setup](./setup.md#basic-setup) (Linux/macOS/Windows): uses [`elan`](https://github.com/Kha/elan) + your preinstalled editor * [Nix setup](./setup.md#nix-setup) (Linux/macOS/WSL): uses the [Nix](https://nixos.org/nix/) package manager for installing all dependencies localized to your project +See also the [quickstart](./quickstart.md) instructions for using the basic setup with VS Code as the editor. + ## Basic Setup Release builds for all supported platforms are available at .