diff --git a/.envrc b/.envrc new file mode 100644 index 0000000..7c7e899 --- /dev/null +++ b/.envrc @@ -0,0 +1,6 @@ +use_flake() { + watch_file flake.nix + watch_file flake.lock + eval "$(nix print-dev-env)" +} +use flake diff --git a/.gitignore b/.gitignore index 796b96d..f59d09f 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1,4 @@ /build +result* +# Do not lock flake to avoid having to maintain it +flake.lock diff --git a/README.md b/README.md index 418118a..29cf643 100644 --- a/README.md +++ b/README.md @@ -13,6 +13,15 @@ $ ./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 + +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`. + +A development environment with lean 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`. + ### Augmenting Lake's Search Path The `lake` executable needs to know where to find the `.olean` files for the modules used in the package configuration file. Lake will intelligently setup an initial search path based on the location of its own executable and `lean`. diff --git a/flake.nix b/flake.nix new file mode 100644 index 0000000..46dd2d6 --- /dev/null +++ b/flake.nix @@ -0,0 +1,52 @@ +{ + description = "Lake (Lean Make) is a new build system and package manager for Lean 4."; + + inputs = { + nixpkgs.url = "github:nixos/nixpkgs/nixos-21.05"; + lean = { + url = "github:leanprover/lean4"; + }; + flake-utils = { + url = "github:numtide/flake-utils"; + inputs.nixpkgs.follows = "nixpkgs"; + }; + }; + + outputs = + { self + , flake-utils + , nixpkgs + , lean + }: + flake-utils.lib.eachDefaultSystem (system: + let + pkgs = import nixpkgs { inherit system; }; + packageName = "Lake"; + src = ./.; + leanPkgs = lean.packages.${system}; + project = leanPkgs.buildLeanPackage { + name = packageName; + inherit src; + }; + in + { + packages.${packageName} = project.lean-package; + packages.lakeProject = project; + + defaultPackage = self.packages.${system}.${packageName}; + + apps.lake = flake-utils.lib.mkApp { + name = "lake"; + drv = project.executable; + }; + + defaultApp = self.apps.${system}.lake; + + # `nix develop` + devShell = pkgs.mkShell { + buildInputs = with pkgs; [ + leanPkgs.lean + ]; + }; + }); +}