-
Notifications
You must be signed in to change notification settings - Fork 45
/
flake.nix
109 lines (87 loc) · 2.97 KB
/
flake.nix
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
103
104
105
106
107
108
109
{
inputs = {
opam-nix.url = "github:tweag/opam-nix";
flake-utils.url = "github:numtide/flake-utils";
nixpkgs.url = "github:nixos/nixpkgs/23.11";
stable.url = "github:nixos/nixpkgs/23.11";
nixpkgs.follows = "opam-nix/nixpkgs";
prover_cvc4_1_8 = {
url = "github:CVC4/CVC4-archived/1.8";
flake = false;
};
prover_cvc5_1_0_5 = {
url = "github:cvc5/cvc5/cvc5-1.0.5";
flake = false;
};
prover_z3_4_12_6 = {
url = "github:z3prover/z3/z3-4.12.6";
flake = false;
};
};
outputs = { self, flake-utils, opam-nix, nixpkgs, ... }@inputs:
let package = "easycrypt"; in
flake-utils.lib.eachDefaultSystem (system:
let
pkgs = nixpkgs.legacyPackages.${system};
on = opam-nix.lib.${system};
devPackagesQuery = {
merlin = "*";
ocaml-lsp-server = "*";
ocamlformat = "*";
};
query = devPackagesQuery // {
ocaml-base-compiler = "4.14.1";
};
scope = on.buildOpamProject' { } ./. query;
overlay = final: prev: {
${package} = prev.${package}.overrideAttrs (oa: {
nativeBuildInputs = oa.nativeBuildInputs
++ pkgs.lib.optionals pkgs.stdenv.isDarwin [ pkgs.darwin.sigtool ];
postInstall = ''
ln -s "$out/lib/ocaml/$opam__ocaml__version/site-lib/easycrypt" $out/lib/
'';
doNixSupport = false;
});
};
scope' = scope.overrideScope' overlay;
# Packages from devPackagesQuery
devPackages = builtins.attrValues
(pkgs.lib.getAttrs (builtins.attrNames devPackagesQuery) scope');
# The main package containing the executable
main = pkgs.symlinkJoin {
name = "main";
paths = [ scope'.${package} scope'.why3 ];
};
# Create provers packages
mkProverPackage = pkg: version:
pkgs.${pkg}.overrideAttrs (_: {
inherit version;
src = inputs."${"prover_" + pkg + "_" + builtins.replaceStrings ["."] ["_"] version}";
});
mkAltErgo = version: (on.queryToScope { } (query // { alt-ergo = version; })).alt-ergo;
in rec {
legacyPackages = scope';
packages = rec {
z3 = mkProverPackage "z3" "4.12.6";
cvc4 = mkProverPackage "cvc4" "1.8";
cvc5 = mkProverPackage "cvc5" "1.0.5";
altErgo = mkAltErgo "2.4.2";
provers = pkgs.symlinkJoin {
name = "provers";
paths = [ altErgo z3 cvc4 cvc5 ];
};
with_provers = pkgs.symlinkJoin {
name = "with-provers";
paths = [ main provers ];
};
default = main;
};
devShells.default = pkgs.mkShell {
inputsFrom = [ scope'.easycrypt ];
buildInputs =
devPackages
++ [ scope'.why3 packages.provers ]
++ (with pkgs.python3Packages; [ pyyaml ]);
};
});
}