perennial/flake.nix at master · mit-pdos/perennial · 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
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
{
  description = "A Flake for Perennial development, with Goose and Grackle";

  inputs = {
    nixpkgs.url = "github:/NixOS/nixpkgs/f61125a668a320878494449750330ca58b78c557";
    flake-utils.url = "github:numtide/flake-utils";
    grackle.url = "github:mjschwenne/grackle";
    opam-nix.url = "github:tweag/opam-nix";
    opam-repository = {
      url = "github:ocaml/opam-repository";
      flake = false;
    };
    opam-rocq-repo = {
      url = "github:rocq-prover/opam";
      flake = false;
    };
  };

  outputs = {
    nixpkgs,
    flake-utils,
    grackle,
    opam-nix,
    opam-repository,
    opam-rocq-repo,
    ...
  }:
    flake-utils.lib.eachDefaultSystem (
      system: let
        pkgs = import nixpkgs {
          inherit system;
        };
        inherit (opam-nix.lib.${system}) buildOpamProject;
        perennialPkgs' =
          buildOpamProject {
            repos = ["${opam-repository}" "${opam-rocq-repo}/released"];
          } "perennial"
          ./. {};
        perennial = perennialPkgs'.perennial.overrideAttrs (finalAttrs: previousAttrs: {
          nativeBuildInputs = with pkgs; [python3] ++ previousAttrs.nativeBuildInputs;
          preBuild = ''
            # swap ROCQPATH for COQPATH, avoiding overriding the complex configurationPhase
            export ROCQPATH=$COQPATH
            unset COQPATH
          '';
          buildPhase = ''
            runHook preBuild
            make -j$NIX_BUILD_CORES all
            runHook postBuild
          '';
          installPhase = ''
            runHook preInstall
            ./etc/install.sh all
            runHook postInstall
          '';
        });
        # remove the perennial package from perennialPkgs since it won't build without python
        perennialPkgs = removeAttrs perennialPkgs' ["perennial"];
      in {
        packages = {
          inherit perennialPkgs perennial;
          default = perennial;
        };
        devShells.default = with pkgs;
          mkShell {
            buildInputs =
              [
                opam
                python3

                go
                grackle.packages.${system}.default
                grackle.packages.${system}.goose
                protobuf

                # nix helpers
                nix-update

                # opam related system dependencies
                pkg-config
                gmp
                findutils
              ]
              ++ (with perennialPkgs; [
                rocq-runtime
                rocq-stdlib
                coq-coqutil
                coq-record-update
                rocq-stdpp
                rocq-iris
                iris-named-props
              ]);

            shellHook = ''
              # swap ROCQPATH for COQPATH
              export ROCQPATH=$COQPATH
              unset COQPATH
            '';
          };
      }
    );
}