From 8cd7efb2d856cadeea26289a3157a21323237a0b Mon Sep 17 00:00:00 2001 From: tydeu Date: Thu, 30 Sep 2021 16:25:58 -0400 Subject: [PATCH] chore: post PR cleanup --- .gitignore | 2 +- README.md | 13 ++++++++----- 2 files changed, 9 insertions(+), 6 deletions(-) diff --git a/.gitignore b/.gitignore index f59d09fc42..1d60dbb262 100644 --- a/.gitignore +++ b/.gitignore @@ -1,4 +1,4 @@ /build result* -# Do not lock flake to avoid having to maintain it +# Do not commit the flake lockfile to avoid having to maintain it flake.lock diff --git a/README.md b/README.md index 52440c87d8..67fed058c3 100644 --- a/README.md +++ b/README.md @@ -13,14 +13,17 @@ $ ./build.sh -j4 After building, the `lake` binary will be located at `build/bin/lake` and the library's `.olean` files will be located directly in `build`. -### Building with nix flakes +### Building with Nix Flakes -It is also possible to build lake with the nix setup `buildLeanPackage` from lean4. To do this you need to have nix installed with flakes enabled. It is recommended to have set up the lean4 binary cache as described in the lean4 repo. -It is then possible to build lake with `nix build .` or run it from anywhere with `nix run github:leanprover/lake`. +It is also possible to build Lake with the Nix setup `buildLeanPackage` from the [`leanprover/lean4`](https://github.com/leanprover/lean4) repository. To do so, you need to have Nix installed with flakes enabled. It is recommended to also set up the Lean 4 binary cache as described in the Lean 4 repository. -A development environment with lean installed can be loaded automatically by running `nix develop` or automatically on `cd` with direnv by running `direnv allow`. +It is then possible to build Lake with `nix build .` or run it from anywhere with `nix run github:leanprover/lake`. -The versions of nixpkgs and lean4 are fixed to specific hashes. They can be updated by running `nix flake update`. +A development environment with Lean 4 installed can be loaded automatically by running `nix develop` or automatically on `cd` with `direnv` by running `direnv allow`. + +The versions of `nixpkgs` and `lean4` are fixed to specific hashes. They can be updated by running `nix flake update`. + +Thank Anders Christiansen Sørby ([@Anderssorby](https://github.com/Anderssorby)) for this support! ### Augmenting Lake's Search Path