-
Notifications
You must be signed in to change notification settings - Fork 1
/
lib.nix
78 lines (71 loc) · 3 KB
/
lib.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
{ ocamlPackages, mkDerivation, lib, makeWrapper, z3, which }:
let
# TODO: we don't need z3 all the time
buildInputs = with ocamlPackages; [
z3 ocaml
# Following F*'s INSTALL.md
ocamlbuild findlib batteries stdint zarith yojson fileutils pprint
menhir menhirLib ppx_deriving ppx_deriving_yojson process
ocaml-migrate-parsetree sedlex
];
preBuild = {name}: ''
echo "echo ${lib.escapeShellArg name}" > src/tools/get_commit
patchShebangs src/tools
patchShebangs ulib # for `gen_mllib.sh`
patchShebangs bin'';
installLibs = ''
mkdir -p $out/lib/ocaml/${ocamlPackages.ocaml.version}/site-lib
for lib in fstar-tactics-lib fstarlib fstar-compiler-lib; do
cp -r "bin/$lib" "$out/bin/$lib"
ln -s "$out/bin/$lib" "$out/lib/ocaml/${ocamlPackages.ocaml.version}/site-lib/$lib"
done
'';
binary-installPhase = { keep_src ? false, withlibs ? true}: ''
mkdir -p $out/ulib/ $out/bin/
cp bin/fstar.exe $out/bin/fstar.exe
cp -r ./ulib/ ${if keep_src then "./src/" else ""} $out/
wrapProgram $out/bin/fstar.exe --prefix PATH ":" "${lib.getBin z3}/bin"
${if withlibs then installLibs else ""}
'';
binary-of-ml-snapshot =
{ src, name, keep_src ? false, withlibs ? true
}: mkDerivation {
inherit name src buildInputs;
nativeBuildInputs = [ makeWrapper ];
buildPhase = ''${preBuild {inherit name;}}
make ${if withlibs then "" else "1"} -j6'';
installPhase = binary-installPhase {inherit keep_src withlibs;};
meta.mainProgram = "fstar.exe";
};
ocaml-from-fstar = { src, name, existing-fstar, patches ? []
}: mkDerivation {
inherit name src patches;
buildInputs = buildInputs ++ [which];
buildPhase = ''
cd bin
test -f fstar-any.sh && {
# we are before commit 6dbcdc1bce
rm fstar-any.sh
ln -s '${existing-fstar}/bin/fstar.exe' fstar-any.sh
}
ln -s '${existing-fstar}/bin/fstar.exe' fstar.exe
cd ..
${preBuild {inherit name;}}
make ocaml -C src -j6
'';
installPhase = ''cp -r . $out'';
};
build =
{ src, name
, keep_src ? false, withlibs ? true, patches ? []
, existing-fstar ? binary-of-ml-snapshot {inherit src; name = "${name}-bin-from-snapshot"; keep_src = true; withlibs = false;}
}:
binary-of-ml-snapshot {
inherit keep_src withlibs name;
src = ocaml-from-fstar {name = "${name}-extracted-fstar"; inherit src existing-fstar patches;};
} // {passthru = {inherit ocamlPackages;};};
in
{
inherit build ocaml-from-fstar binary-of-ml-snapshot buildInputs
binary-installPhase installLibs;
}