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

doc: Nix: explain some warnings

Browse source 
/cc @leodemoura @javra
This commit is contained in:
Sebastian Ullrich 2020-11-24 12:15:06 +01:00
parent bc0010b84c
commit 4f89cbf9b9
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
doc/make/nix.md
View file

@ -25,6 +25,8 @@ sudo mkdir -m0770 -p /nix/var/cache/ccache
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:
@ -42,6 +44,8 @@ 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.
Note: Nix will print a warning "Git tree [...] is dirty" when you have uncommitted changes as a reminder that you're not building the "actual repo contents", but the message is otherwise harmless.
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