Add a nix flake setup

.envrc

@@ -0,0 +1,6 @@
+use_flake() {
+  watch_file flake.nix
+  watch_file flake.lock
+  eval "$(nix print-dev-env)"
+}
+use flake

.gitignore

@@ -1 +1,4 @@
 /build
+result*
+# Do not lock flake to avoid having to maintain it
+flake.lock

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`.

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
+        ];
+      };
+    });
+}