koika/flake.nix at master · epfl-systemf/koika · 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
{
  description = "A core language for rule-based hardware design";

  inputs = {
    flake-utils.url = "github:numtide/flake-utils";
    nixpkgs.url = "github:nixos/nixpkgs/release-25.05";
  };

  outputs = { self, flake-utils, nixpkgs, ... }:
    let koikaPkg = { pkgs, lib, mkCoqDerivation, coq, boost, doCheck ? false, }:
      mkCoqDerivation rec {
        pname = "koika";
        defaultVersion = "0.0.1";

        # derivation is build using "dune build -p {opam-name}"
        opam-name = "koika";
        useDune = true;

        release."0.0.1" = {
          src = lib.cleanSourceWith {
            src = lib.cleanSource ./.;
            filter = let inherit (lib) all hasSuffix; in
              path: _: all (x: !hasSuffix x path) [
                "flake.nix"
                ".gitignore"
              ];
            };
        };

        enableParallelBuilding = true;

        # run-time dependencies
        buildInputs = [
          boost
        ];

        nativeBuildInputs = with pkgs; [
          gnumake git bash
        ];

        # Coq/ocaml libraries and Coq plugins (necessary to propagate PATH)
        propagatedBuildInputs = with coq.ocamlPackages; [
          findlib
          base
          core
          core_unix
          stdio
          parsexp
          hashcons
          zarith
        ];

        configurePhase = ''
          make configure
        '';

        inherit doCheck;
        checkPhase = ''
          runHook preCheck
          make all
          runHook postCheck
        '';
      }; in
    flake-utils.lib.eachDefaultSystem (system:
      let pkgs = import nixpkgs {
        inherit system;
        overlays = [ self.overlays.default ];
      }; in rec {
        checks = {
          koika = packages.default.override { doCheck = true; };
        };

        devShells.default = packages.default;

        packages = rec {
          default = coq8_18-koika;
          coq8_18-koika = pkgs.coqPackages_8_18.koika;
        };
      }
    )
    // {
      # NOTE: To use this flake, apply the following overlay to nixpkgs and use
      # koika from its respective coqPackages_VER attribute set!
      overlays.default = final: prev:
        prev.lib.mapAttrs (name: _:
          prev.${name}.overrideScope (
            self: _: { koika = self.callPackage koikaPkg { }; }
          )
        ) {
          inherit (final) coqPackages_8_18;
        };
    };
}