diff --git a/doc/SUMMARY.md b/doc/SUMMARY.md index 406c7ecdc8..f2904e46d5 100644 --- a/doc/SUMMARY.md +++ b/doc/SUMMARY.md @@ -4,7 +4,6 @@ - [Tour of Lean](./tour.md) - [Setting Up Lean](./quickstart.md) - [Extended Setup Notes](./setup.md) - - [Nix Setup](./setup/nix.md) - [Theorem Proving in Lean](./tpil.md) - [Functional Programming in Lean](fplean.md) - [Examples](./examples.md) @@ -86,7 +85,6 @@ - [macOS Setup](./make/osx-10.9.md) - [Windows MSYS2 Setup](./make/msys2.md) - [Windows with WSL](./make/wsl.md) - - [Nix Setup (*Experimental*)](./make/nix.md) - [Bootstrapping](./dev/bootstrap.md) - [Testing](./dev/testing.md) - [Debugging](./dev/debugging.md) diff --git a/doc/dev/testing.md b/doc/dev/testing.md index 8f427a6417..3c4fb197c5 100644 --- a/doc/dev/testing.md +++ b/doc/dev/testing.md @@ -124,8 +124,3 @@ outputs. `meld` can also be used to repair the problems. In Emacs, we can also execute `M-x lean4-diff-test-file` to check/diff the file of the current buffer. To mass-copy all `.produced.out` files to the respective `.expected.out` file, use `tests/lean/copy-produced`. -When using the Nix setup, add `--keep-failed` to the `nix build` call and then call -```sh -tests/lean/copy-produced /source/tests/lean -``` -instead where `` is the path printed out by `nix build`. diff --git a/doc/make/index.md b/doc/make/index.md index 1e6e4dbd84..eba03bdd7f 100644 --- a/doc/make/index.md +++ b/doc/make/index.md @@ -14,8 +14,6 @@ Platform-Specific Setup - [Windows (WSL)](wsl.md) - [macOS (homebrew)](osx-10.9.md) - Linux/macOS/WSL via [Nix](https://nixos.org/nix/): Call `nix-shell` in the project root. That's it. -- There is also an [**experimental** setup based purely on Nix](nix.md) that works fundamentally differently from the - make/CMake setup described on this page. Generic Build Instructions -------------------------- diff --git a/doc/make/nix.md b/doc/make/nix.md deleted file mode 100644 index 9e161e8674..0000000000 --- a/doc/make/nix.md +++ /dev/null @@ -1,110 +0,0 @@ -# Building with Nix - -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 - -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 -``` - -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. -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 -``` - -## Basic Build Commands - -From the Lean root directory inside the Lean shell: -```bash -nix build .#stage1 # build this stage's stdlib & executable -nix build .#stage1.test # run all tests -nix run .#stage1.update-stage0 # update ./stage0 from this stage -nix run .#stage1.update-stage0-commit # ...and commit the results -``` -The `stage1.` part in each command is optional: -```bash -nix build .#test # run tests for stage 1 -nix build . # build stage 1 -nix build # ditto -``` - -## Build Process Description - -The Nix build process conceptually works the same as described in [Lean Build Pipeline](index.md#lean-build-pipeline). -However, there are two important differences in practice apart from the standard Nix properties (hermeneutic, reproducible builds stored in a global hash-indexed store etc.): -* Only files tracked by git (using `git add` or at least `git add --intent-to-add`) are compiled. -This is actually a general property of Nix flakes, and has the benefit of making it basically impossible to forget to commit a file (at least in `src/`). -* Only files reachable from `src/Lean.lean` are compiled. -This is because modules are discovered not from a directory listing anymore but by recursively compiling all dependencies of that top module. - -## Editor Integration - -As in the standard Nix setup. -After adding `src/` as an LSP workspace, it should automatically fall back to using stage 0 in there. - -Note that the UX of `{emacs,vscode}-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. -However, it will only ever load changes saved to disk, not ones opened in other buffers. - -The absence of a mutable output directory also means that the Lean server will not automatically pick up `.ilean` metadata from newly compiled files. -Instead, you can run `nix run .#link-ilean` to symlink the `.ilean` tree of the stdlib state at that point in time to `src/build/lib`, where the server should automatically find them. - -## Other Fun Stuff to Do with Nix - -Open Emacs with Lean set up from an arbitrary commit (without even cloning Lean beforehand... if your Nix is new enough): -```bash -nix run github:leanprover/lean4/7e4edeb#emacs-package -``` - -Open a shell with `lean` and `LEAN_PATH` set up for compiling a specific module (this is exactly what `emacs-dev` is doing internally): -```bash -nix develop .#mods.\"Lean.Parser.Basic\" -# alternatively, directly pass a command to execute: -nix develop .#stage2.mods.\"Init.Control.Basic\" -c bash -c 'lean $src -Dtrace.Elab.command=true' -``` - -Not sure what you just broke? Run Lean from (e.g.) the previous commit on a file: -```bash -nix run .\?rev=$(git rev-parse @^) scratch.lean -``` - -Work on two adjacent stages at the same time without the need for repeatedly updating and reverting `stage0/`: -```bash -# open an editor that will use only committed changes (so first commit them when changing files) -nix run .#HEAD-as-stage1.emacs-dev& -# open a second editor that will use those committed changes as stage 0 -# (so don't commit changes done here until you are done and ran a final `update-stage0-commit`) -nix run .#HEAD-as-stage0.emacs-dev& -``` -To run `nix build` on the second stage outside of the second editor, use -```bash -nix build .#stage0-from-input --override-input lean-stage0 .\?rev=$(git rev-parse HEAD) -``` -This setup will inadvertently change your `flake.lock` file, which you can revert when you are done. - -...more surely to come... - -## Debugging - -Since Nix copies all source files before compilation, you will need to map debug symbols back to the original path using `set substitute-path` in GDB. -For example, for a build on Linux with the Nix sandbox activated: -```bash -(gdb) f -#1 0x0000000000d23a4f in lean_inc (o=0x1) at /build/source/build/include/lean/lean.h:562 -562 /build/source/build/include/lean/lean.h: No such file or directory. -(gdb) set substitute-path /build/source/build src -(gdb) f -#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); } -``` diff --git a/doc/setup/nix.md b/doc/setup/nix.md deleted file mode 100644 index 9522c58799..0000000000 --- a/doc/setup/nix.md +++ /dev/null @@ -1,71 +0,0 @@ -# Nix Setup - -An 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. -However, 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 (), 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. -Such packages follow the same directory layout as described in the standard setup, except for a `lakefile.lean` replaced by a `flake.nix` file 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 (after you've added one) -$ 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 -$ nix run .#vscode-dev MyPackage.lean # ditto, using VS Code -``` -Note that if you rename `MyPackage.lean`, you also have to adjust the `name` attribute in `flake.nix` accordingly. -Also note that if you turn the package into a Git repository, only tracked files will be visible to Nix. - -As in the standard setup, changes need to be saved to be visible in other files, which have then to be invalidated via an editor command. - -If you don't want to or cannot start the pinned editor from Nix, e.g. because you're running Lean inside WSL/a container/on a different machine, you can manually point your editor at the `lean` wrapper script the commands above use internally: -```bash -$ nix build .#lean-dev -o result-lean-dev -``` -The resulting `./result-lean-dev/bin/lean` script essentially runs `nix run .#lean` in the current project's root directory when you open a Lean file or use the "refresh dependencies" command such that the correct Lean version for that project is executed. -This includes selecting the correct stage of Lean (which it will compile on the fly, though without progress output) if you are [working on Lean itself](./make/nix.md#editor-integration). - -Package dependencies can be added as further input flakes and passed to the `deps` list of `buildLeanPackage`. Example: - -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 `lakefile.lean` used in the standard setup. -Unifying the two formats is TBD.