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

chore: post PR cleanup

Browse source
This commit is contained in:
tydeu 2021-09-30 16:25:58 -04:00
parent cadc812608
commit 8cd7efb2d8
2 changed files with 9 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
.gitignore vendored
View file

@ -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

13
README.md
View file

@ -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