tjh.dev
1{
2 stdenv,
3 lib,
4 ocaml,
5 findlib,
6 zarith,
7 z3,
8}:
9
10if lib.versionOlder ocaml.version "4.08" then
11 throw "z3 is not available for OCaml ${ocaml.version}"
12else
13
14 let
15 z3-with-ocaml = (
16 z3.override {
17 ocamlBindings = true;
18 inherit ocaml findlib zarith;
19 }
20 );
21 in
22
23 stdenv.mkDerivation {
24
25 pname = "ocaml${ocaml.version}-z3";
26 inherit (z3-with-ocaml) version;
27
28 dontUnpack = true;
29
30 installPhase = ''
31 runHook preInstall
32 mkdir -p $OCAMLFIND_DESTDIR
33 cp -r ${z3-with-ocaml.ocaml}/lib/ocaml/${ocaml.version}/site-lib/stublibs $OCAMLFIND_DESTDIR
34 cp -r ${z3-with-ocaml.ocaml}/lib/ocaml/${ocaml.version}/site-lib/Z3 $OCAMLFIND_DESTDIR/z3
35 runHook postInstall
36 '';
37
38 nativeBuildInputs = [ findlib ];
39 propagatedBuildInputs = [
40 z3-with-ocaml.lib
41 zarith
42 ];
43
44 strictDeps = true;
45
46 meta = z3.meta // {
47 description = "Z3 Theorem Prover (OCaml API)";
48 };
49 }