From 4f89cbf9b9a3b077ca58257c118555b019efefe5 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 24 Nov 2020 12:15:06 +0100 Subject: [PATCH] doc: Nix: explain some warnings /cc @leodemoura @javra --- doc/make/nix.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/doc/make/nix.md b/doc/make/nix.md index f1f264489e..01dee7168e 100644 --- a/doc/make/nix.md +++ b/doc/make/nix.md @@ -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