-
Notifications
You must be signed in to change notification settings - Fork 0
/
default.nix
127 lines (122 loc) · 3.5 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
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
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
{lib, stdenv, which, fstar, fstar-dune, z3, nodejs_20, ocamlPackages, comparse, dolev-yao-star, hacl-packages-src, fetchFromGitHub}:
let
mls-star = stdenv.mkDerivation {
name = "mls-star";
src =
lib.sources.sourceByRegex ./. [
"Makefile"
"hacl-star-snapshot"
"hacl-star-snapshot/lib(/.*)?"
"hacl-star-snapshot/specs(/.*)?"
# Include all the F* files, except the ones in fstar/test
# The directory fstar/test has to be created though, as it is hardcoded in the makefile
"fstar"
"fstar/test"
"fstar/(api|bootstrap|common|glue|symbolic|treedem|treekem|treemath|treesync).*"
]
;
enableParallelBuilding = true;
buildInputs = [ which fstar z3 ];
COMPARSE_HOME = comparse;
DY_HOME = dolev-yao-star;
installPhase = ''
mkdir -p $out
cp -r ml fstar cache hints $out
'';
passthru.tests = mls-star-tests;
passthru.js = mls-star-js;
};
mls-star-tests = stdenv.mkDerivation {
name = "mls-star-tests";
src =
lib.sources.sourceByRegex ./. [
"hacl-star-snapshot(/.*)?"
"fstar(/.*)?"
"Makefile"
"dune-project"
"ml(/lib(/dune)?)?"
"ml(/tests(/dune)?)?"
"mls.opam"
"test_vectors(/git_commit)?"
]
;
enableParallelBuilding = true;
buildInputs =
[ which fstar z3 ]
++ (with ocamlPackages; [
ocaml dune_3 findlib yojson hacl-star
])
++ (fstar-dune.buildInputs);
COMPARSE_HOME = comparse;
DY_HOME = dolev-yao-star;
# pre-patch uses build output from mls-star, to avoid building things twice
prePatch = ''
cp -pr --no-preserve=mode ${mls-star}/cache ${mls-star}/ml .
mkdir obj
cp -p ml/lib/src/* obj/
mkdir -p test_vectors/data
cp -pr --no-preserve=mode ${test-files}/test-vectors/* test_vectors/data
'';
doCheck = true;
installPhase = ''
mkdir -p $out
cp -r ml fstar cache hints $out
'';
passthru.test-vectors = test-files;
};
test-rev = builtins.replaceStrings ["\n"] [""] (builtins.readFile ./test_vectors/git_commit);
test-files =
fetchFromGitHub {
owner = "mlswg";
repo = "mls-implementations";
rev = test-rev;
sha256 = "sha256-qYtSzY9epzvgahbJ3/omzGRwH5PVDLQmFfHzmQLDRc8=";
}
;
mls-star-js = stdenv.mkDerivation {
name = "mls-star-js";
src =
lib.sources.sourceByRegex ./. [
"hacl-star-snapshot(/.*)?"
"fstar(/.*)?"
"Makefile"
"dune-project"
"ml(/lib(/dune)?)?"
"ml(/tests(/dune)?)?"
"js(/.*)?"
"mls.opam"
]
;
enableParallelBuilding = true;
# pre-patch uses build output from mls-star, to avoid building things twice
prePatch = ''
patchShebangs js/import.sh
cp -pr --no-preserve=mode ${mls-star-tests}/cache ${mls-star-tests}/ml .
mkdir obj
cp -p ml/lib/src/* obj/
'';
buildPhase = ''
make js
'';
doCheck = true;
checkPhase = ''
(cd js; node test.js)
'';
installPhase = ''
mkdir $out
# Remove the date for reproducible builds
cp mls-*.tar.bz2 $out/mls.tar.bz2
'';
buildInputs =
[ which fstar z3 nodejs_20 ]
++ (with ocamlPackages; [
ocaml dune_3 findlib yojson hacl-star
js_of_ocaml js_of_ocaml-ppx integers_stubs_js
])
++ (fstar-dune.buildInputs);
COMPARSE_HOME = comparse;
DY_HOME = dolev-yao-star;
HACL_PACKAGES_HOME = hacl-packages-src;
};
in
mls-star