sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 18:34:06 +00:00
Code Issues Packages Projects Releases Wiki Activity

doc: elaborate on elan setup

Browse Source
This commit is contained in:
Sebastian Ullrich
2020-05-15 21:20:00 +02:00
parent e6463903d8
commit bb554930f8
1 changed files with 34 additions and 12 deletions
Download Patch File Download Diff File Expand all files Collapse all files

46
doc/make/index.md
View File

@@ -144,26 +144,48 @@ After building a stage, you can invoke `make -C stageN test` (or, even better,
`make test` without `-C` defaults to stage 0.5. While the Lean tests
will automatically use that stage's corresponding Lean executables, for running
tests or compiling Lean programs manually, you need to put them into your `PATH`
yourself. A simple option for doing that is to register them as custom toolchains
in [`elan`](https://github.com/Kha/elan):
```
# in the Lean rootdir
elan toolchain link lean4 build/release/stage0.5
# make `lean` etc. point to the given build in the rootdir and subdirs
elan override set lean4
```
You can also use the `+toolchain` shorthand (e.g. `lean +lean4-debug`) to switch
toolchains on the spot.
yourself. A simple option for doing that is to use
[`elan`](https://github.com/Kha/elan), see the next section.
The only currently supported editor is Emacs, see `lean4-mode/README.md` for
basic setup. You can set `lean4-rootdir` manually to tell it what stage to use,
but `elan` again makes it simple to do that automatically, e.g. using stage 0
for editing the stdlib while using a different stage for all other files:
but `elan` again makes it simple to do that automatically.
Dev setup using elan
--------------------
You can use [`elan`](https://github.com/Kha/elan) to easily switch between
stages and build configurations based on the current directory, both for the
`lean/leanc/leanmake` binaries in your shell's PATH and inside Emacs.
If you haven't already installed elan, you can do so, without installing a
default version of Lean, using
```bash
curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none
```
You can use `elan toolchain link` to give a specific stage build directory a
reference name, then use `elan override set` to associate such a name to the
current directory. We usually want to use `stage0` for editing files in `src`
and `stage0.5` for everything else (e.g. tests).
```
# in the Lean rootdir
elan toolchain link lean4 build/release/stage0.5
elan toolchain link lean4-stage0 build/release/stage0
# make `lean` etc. point to stage0.5 in the rootdir and subdirs
elan override set lean4
cd src
# make `lean` etc. point to stage0 anywhere inside `src`
elan override set lean4-stage0
```
You can also use the `+toolchain` shorthand (e.g. `lean +lean4-debug`) to switch
toolchains on the spot. `lean4-mode` will automatically use the `lean` executable
associated with the directory of the current file as long as `lean4-rootdir` is
unset and `~/.elan/bin` is in your `exec-path`.
You might find that debugging through elan, e.g. via `gdb lean`, disables some
things like symbol autocompletion because at first only the elan proxy binary
is loaded. You can instead pass the explicit path to `bin/lean` in your build
folder to gdb, or use `gdb $(elan which lean)`.
Troubleshooting
---------------