max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: quickstart

Browse source
This commit is contained in:
Sebastian Ullrich 2021-04-06 17:34:01 +02:00
parent 3438f425f1
commit dcfd6f4873
4 changed files with 24 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

BIN
doc/images/code-ext.png Normal file
View file

Binary file not shown.
Side by side

After

Width:  |  Height:  |  Size: 12 KiB

BIN
doc/images/code-success.png Normal file
View file

Binary file not shown.
Side by side

After

Width:  |  Height:  |  Size: 18 KiB

22
doc/quickstart.md Normal file
View file

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

2
doc/setup.md
View file

@ -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 <https://github.com/leanprover/lean4/releases>.