lean4-nix/flake.nix at main · lenianiva/lean4-nix · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
{
  description = "Lean 4 Nix Flake";

  inputs = {
    nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable";
    flake-parts.url = "github:hercules-ci/flake-parts";
  };

  outputs = inputs @ {
    self,
    nixpkgs,
    flake-parts,
    ...
  }:
    flake-parts.lib.mkFlake {inherit inputs;} {
      systems = [
        "aarch64-darwin"
        "aarch64-linux"
        "x86_64-darwin"
        "x86_64-linux"
      ];

      flake =
        (import ./lib/overlay.nix)
        // {
          lake = import ./lib/lake.nix;
          templates = import ./templates;
        };

      perSystem = {
        system,
        pkgs,
        ...
      }: let
        toolchain-file = ./templates/minimal/lean-toolchain;
        # With built toolchain
        pkgs-bin = import nixpkgs {
          inherit system;
          overlays = [(self.readToolchainFile toolchain-file)];
        };
        # With binary toolchain
        pkgs = import nixpkgs {
          inherit system;
          overlays = [
            (self.readToolchainFile {
              toolchain = toolchain-file;
              binary = false;
            })
          ];
        };
        lake2nix-bin = pkgs-bin.callPackage self.lake {};
      in {
        packages = {
          lean-bin = pkgs-bin.lean;
          inherit (pkgs) lean;
          inherit (pkgs.lean) cacheRoots;
          inherit (pkgs.callPackage ./lib/toolchain.nix {}) toolchain-fetch;
        };
        devShells.default = pkgs.mkShell {
          buildInputs = [pkgs.prek];
        };

        checks = (import ./checks.nix) {inherit pkgs-bin lake2nix-bin pkgs;};

        formatter = pkgs.alejandra;
      };
    };
}