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

doc: setup

Browse source
This commit is contained in:
Sebastian Ullrich 2021-01-02 22:22:44 +01:00
parent 626ff28e0e
commit 9485b8d074
5 changed files with 98 additions and 62 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
default.nix
View file

@ -1,3 +1,5 @@
# used for `nix-shell https://github.com/leanprover/lean4/archive/master.tar.gz -A nix`
{ nix = (import ./shell.nix {}).nix; } //
(import (
fetchTarball {
url = "https://github.com/edolstra/flake-compat/archive/c75e76f80c57784a6734356315b306140646ee84.tar.gz";

1
doc/SUMMARY.md
View file

@ -2,6 +2,7 @@
- [What is Lean](./whatIsLean.md)
- [Tour of Lean](./tour.md)
- [Setting Up Lean](./setup.md)
# Language Manual

3
doc/faq.md
View file

@ -41,8 +41,7 @@ make sure that Lean attends all your needs. You should not expect we will fix bu
* Are there IDEs for Lean?
We currently have a very simple [Emacs mode](https://github.com/leanprover/lean4/tree/master/lean4-mode) for Lean 4.
Lean 3 supports many IDEs, the two main ones are for [Emacs](https://github.com/leanprover/lean-mode) and [VS Code](https://github.com/leanprover/vscode-lean).
Yes, see [Setting Up Lean](./setup.md).
* Is Lean sound? How big is the kernel? Should I trust it?

69
doc/make/nix.md
View file

@ -1,37 +1,25 @@
While [Nix](https://nixos.org/nix/) can be used to quickly open a shell with all dependencies for the [standard setup](index.md) installed, we also support a setup based purely on Nix, though it is still experimental; in particular, it is heavily based on an unreleased version of Nix enabling [Nix Flakes](https://www.tweag.io/blog/2020-05-25-flakes/). The setup has been tested on NixOS, other Linux distributions, and macOS.
While [Nix](https://nixos.org/nix/) can be used to quickly open a shell with all dependencies for the [standard setup](index.md) installed, the user-facing [Nix Setup](../setup.md#nix-setup) can also be used to work *on* Lean.
# Setup
After installing (any version of) Nix ([https://nixos.org/download.html]), you can easily open a shell with the particular pre-release version of Nix needed by and tested with our setup (called the "Lean shell" from here on):
Follow the setup in the link above; to open the Lean shell inside a Lean checkout, you can also use
```bash
# in the Lean root directory
$ nix-shell -A nix
```
While this shell is sufficient for executing the steps below, it is recommended to also set the following options in `/etc/nix/nix.conf` (`nix.extraOptions` in NixOS):
```
max-jobs = auto # Allow building multiple derivations in parallel
keep-outputs = true # Do not garbage-collect build time-only dependencies (e.g. clang)
extra-sandbox-paths = /nix/var/cache/ccache # Extra local cache for C/C++ code
# Allow fetching build results from the Lean Cachix cache
trusted-substituters = https://lean4.cachix.org/
trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= lean4.cachix.org-1:mawtxSxcaiWE24xCXXgh3qnvlTkyU7evRRnGeAhD4Wk=
```
On a multi-user installation of Nix (the default), you need to restart the Nix daemon afterwards:
```bash
sudo pkill nix-daemon
```
The [Cachix](https://cachix.org/) integration will magically beam any build steps already executed by the CI right onto your machine when calling Nix commands in the shell opened above.
On top of the local and remote Nix cache, we do still rely on CCache as well to make C/C++ build steps incremental, which are atomic steps from Nix's point of view.
If you add the `extra-sandbox-paths` line above, you **must** also set up that directory as follows:
On top of the local and remote Nix cache, it helps to we do still rely on CCache as well to make C/C++ build steps incremental, which are atomic steps from Nix's point of view.
To enable CCache, add the following line to the config file mentioned in the setup:
```bash
extra-sandbox-paths = /nix/var/cache/ccache
```
Then set up that directory as follows:
```bash
sudo mkdir -m0770 -p /nix/var/cache/ccache
# macOS standard chown doesn't support --reference
nix shell .#nixpkgs.coreutils -c sudo chown --reference=/nix/store /nix/var/cache/ccache
```
Note: Your system Nix might print warnings about not knowing some of these settings, which can be ignored.
# Basic Build Commands
From the Lean root directory inside the Lean shell:
@ -47,13 +35,6 @@ nix build .#test # run tests for stage 1
nix build . # build stage 1
nix build # dito
```
On a build error, Nix will show the last 10 lines of the output by default. You can pass `-L` to `nix build` to show all lines, or pass the shown `*.drv` path to `nix log` to show the full log after the fact.
Keeping all outputs ever built on a machine alive can accumulate to quite impressive amounts of disk space, so you might want to trigger the Nix GC when /nix/store/ has grown too large:
```bash
nix-collect-garbage
```
This will remove everything not reachable from "GC roots" such as the `./result` symlink created by `nix build`, so you might want to call that first to keep your current stage 1 alive.
# Build Process Description
@ -66,19 +47,9 @@ This is because modules are discovered not from a directory listing anymore but
# Emacs Integration
Starting a known-good (pinned) version of Emacs from the Lean shell with `lean4-mode` fully set up for development on Lean is as easy as:
```bash
nix run .#emacs-dev
```
As in the standard Nix setup.
After adding `src/` as an LSP workspace using `lsp-workspace-folder-add`, it should automatically fall back to using stage 0 in there.
If you've already installed lean4-mode manually, you might need to first deactivate that. `elan` can be left as is on the other hand.
Arguments can be passed as well:
```bash
nix run .#emacs-dev src/Lean.lean
```
Note that the UX of `emacs-dev` is quite different from the Make-based setup regarding the compilation of dependencies:
there is no mutable directory incrementally filled by the build that we could point the editor at for .olean files.
Instead, `emacs-dev` will gather the individual dependency outputs from the Nix store when checking a file -- and build them on the fly when necessary.
@ -132,25 +103,3 @@ For example, for a build on Linux with the Nix sandbox activated:
#1 0x0000000000d23a4f in lean_inc (o=0x1) at /build/source/build/include/lean/lean.h:562
562 static inline void lean_inc(lean_object * o) { if (!lean_is_scalar(o)) lean_inc_ref(o); }
```
# Building Lean Packages with Nix
From a Lean shell, run
```bash
$ nix flake new mypkg -t github:leanprover/lean4
```
to create a new Lean package in directory `mypkg`.
The Lean package comes with a package root file `MyPackage.lean` and a `flake.nix` set up so you can run most command from above on your own package.
In particular, you can run `nix run .#emacs-dev` in the package directory to start Emacs configured to automatically build and provide any intra- and extra-package dependencies on the fly.
Note that if you rename `MyPackage.lean`, you also have to adjust the `name` attribute in `flake.nix` accordingly.
Package dependencies can be added as further input flakes and passed to the `deps` list of `buildLeanPackage`. Example: https://github.com/Kha/testpkg2/blob/master/flake.nix
For hacking, it can be useful to temporarily override an input with a local checkout/different version of a dependency:
```bash
$ nix build --override-input somedep path/to/somedep
```
In the future, we would like to introduce a simpler, more generic package description file akin to Lean 3's `leanpkg.toml` that is not Nix-specific and can be produced and consumed by other package manager implementations.
It should be possible to consume it with `builtins.fromTOML` in the Nix setup.

85
doc/setup.md Normal file
View file

@ -0,0 +1,85 @@
# Setting Up Lean
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
## Basic Setup
Release builds for all supported platforms are available at <https://github.com/leanprover/lean4/releases>.
Instead of downloading these and setting up the paths manually, however, it is recommended to use the Lean version manager [`elan`](https://github.com/Kha/elan) instead:
```sh
# download & activate latest Lean 4 release
$ elan default leanprover/lean4:stable
# alternatively, use the latest nightly build
$ elan default leanprover/lean4:nightly
# alternatively, activate Lean 4 in current directory only
$ elan override leanprover/lean4:stable
```
Lean 4 comes with a basic package manager `leanpkg` that mostly works [as in Lean 3](https://leanprover.github.io/reference/using_lean.html#using-the-package-manager).
Note however that it currently depends on `make` (and `sh`) for recursive compilation.
It has been tested on Windows by installing these tools using [MSYS2](https://www.msys2.org/), but [MinGW](http://www.mingw.org/) or WSL should work, too.
Lean implements the [Language Server Protocol](https://microsoft.github.io/language-server-protocol/) that can be used for interactive development in [Emacs](https://github.com/leanprover/lean4/tree/master/lean4-mode/README.md), [VS Code](https://github.com/mhuisi/vscode-lean4), and possibly other editors.
## Nix Setup
The alternative setup based on Nix provides a perfectly reproducible development environment for your project from the Lean version down to the editor and Lean extension. Howeover, it is still experimental and subject to change; in particular, it is heavily based on an unreleased version of Nix enabling [Nix Flakes](https://www.tweag.io/blog/2020-05-25-flakes/). The setup has been tested on NixOS, other Linux distributions, and macOS.
After installing (any version of) Nix (<https://nixos.org/download.html>), you can easily open a shell with the particular pre-release version of Nix needed by and tested with our setup (called the "Lean shell" from here on):
```bash
$ nix-shell https://github.com/leanprover/lean4/archive/master.tar.gz -A nix
```
While this shell is sufficient for executing the steps below, it is recommended to also set the following options in `/etc/nix/nix.conf` (`nix.extraOptions` in NixOS):
```
max-jobs = auto # Allow building multiple derivations in parallel
keep-outputs = true # Do not garbage-collect build time-only dependencies (e.g. clang)
# Allow fetching build results from the Lean Cachix cache
trusted-substituters = https://lean4.cachix.org/
trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= lean4.cachix.org-1:mawtxSxcaiWE24xCXXgh3qnvlTkyU7evRRnGeAhD4Wk=
```
On a multi-user installation of Nix (the default), you need to restart the Nix daemon afterwards:
```bash
sudo pkill nix-daemon
```
The [Cachix](https://cachix.org/) integration will magically beam any build steps already executed by the CI right onto your machine when calling Nix commands in the shell opened above.
It can be set up analogously as a cache for your own project.
Note: Your system Nix might print warnings about not knowing some of the settings used by the Lean shell Nix, which can be ignored.
### Basic Commands
From a Lean shell, run
```bash
$ nix flake new mypkg -t github:leanprover/lean4
```
to create a new Lean package in directory `mypkg` using the latest commit of Lean 4.
The Lean package comes with a package root file `MyPackage.lean` and a `flake.nix` set up so you can run Nix commands on it, for example:
```bash
$ nix build # build package and all dependencies
$ nix build .#executable # compile `main` definition into executable
$ nix run .#emacs-dev # open a pinned version of Emacs with lean4-mode fully set up
$ nix run .#emacs-dev MyPackage.lean # arguments can be passed as well, e.g. the file to open
```
Note that if you rename `MyPackage.lean`, you also have to adjust the `name` attribute in `flake.nix` accordingly.
Package dependencies can be added as further input flakes and passed to the `deps` list of `buildLeanPackage`. Example: <https://github.com/Kha/testpkg2/blob/master/flake.nix#L5>
For hacking, it can be useful to temporarily override an input with a local checkout/different version of a dependency:
```bash
$ nix build --override-input somedep path/to/somedep
```
On a build error, Nix will show the last 10 lines of the output by default. You can pass `-L` to `nix build` to show all lines, or pass the shown `*.drv` path to `nix log` to show the full log after the fact.
Keeping all outputs ever built on a machine alive can accumulate to quite impressive amounts of disk space, so you might want to trigger the Nix GC when `/nix/store/` has grown too large:
```bash
nix-collect-garbage
```
This will remove everything not reachable from "GC roots" such as the `./result` symlink created by `nix build`.
Note that the package information in `flake.nix` is currently completely independent from `leanpkg.toml` used in the basic setup.
Unifying the two formats is TBD.