-
Notifications
You must be signed in to change notification settings - Fork 57
/
default.nix
79 lines (67 loc) · 2.16 KB
/
default.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
{ pkgs ? import (if pinned-nixpkgs then scripts/nixpkgs.nix else <nixpkgs>) {}
, inCI ? false
, pinned-nixpkgs ? inCI
, coqDeps ? !inCI
, coqMaster ? false
, ocamlDeps ? !inCI
, testDeps ? !inCI
, devTools ? !inCI
, ecRef ? ""
, opamDeps ? false
, enableFramePointers ? false
}:
with pkgs;
let inherit (lib) optionals; in
let coqPackages =
if coqMaster then
pkgs.coqPackages.overrideScope (self: super: {
coq = super.coq.override { version = "master"; };
stdlib = super.stdlib.override { version = "master"; };
coq-elpi = callPackage scripts/coq-elpi.nix {
version = "master";
inherit (self) lib mkCoqDerivation coq stdlib;
};
hierarchy-builder = super.hierarchy-builder.override { version = "master"; };
})
else coqPackages_8_19
; in
let mathcomp-word = callPackage scripts/mathcomp-word.nix { inherit coqPackages; }; in
let easycrypt = callPackage scripts/easycrypt.nix {
inherit ecRef;
why3 = pkgs.why3.override { ideSupport = false; };
}; in
let inherit (coqPackages.coq) ocamlPackages; in
let oP =
if enableFramePointers
then ocamlPackages.overrideScope' (self: super: {
ocaml = super.ocaml.overrideAttrs (o: {
configureFlags = o.configureFlags ++ [ "--enable-frame-pointers" ];
});
})
else ocamlPackages
; in
if !lib.versionAtLeast oP.ocaml.version "4.11"
then throw "Jasmin requires OCaml ≥ 4.11"
else
let ecDeps = ecRef != ""; in
stdenv.mkDerivation {
name = "jasmin-0";
src = nix-gitignore.gitignoreSource [] ./.;
buildInputs = []
++ optionals coqDeps [ coqPackages.coq mathcomp-word ]
++ optionals testDeps ([ curl.bin oP.apron.out libllvm ] ++ (with python3Packages; [ python pyyaml ]))
++ optionals ocamlDeps ([ mpfr ppl ] ++ (with oP; [
ocaml findlib dune_3
cmdliner
angstrom
batteries
menhir (oP.menhirLib or null) zarith camlidl apron yojson ]))
++ optionals devTools (with oP; [ merlin ocaml-lsp ])
++ optionals ecDeps [ easycrypt alt-ergo.bin z3.out ]
++ optionals opamDeps [ rsync git pkg-config perl ppl mpfr opam ]
;
enableParallelBuilding = true;
installPhase = ''
make -C compiler install PREFIX=$out
'';
}