ocamlPackages.z3: init at 4.8.9

3 files changed, 49 insertions, 2 deletions

diff --git a/pkgs/applications/science/logic/z3/default.nix b/pkgs/applications/science/logic/z3/default.nix
index 84c1544071ff..88aafcdae222 100644
--- a/pkgs/applications/science/logic/z3/default.nix
+++ b/pkgs/applications/science/logic/z3/default.nix
@@ -1,10 +1,13 @@
 { stdenv, fetchFromGitHub, python, fixDarwinDylibNames
 , javaBindings ? false
+, ocamlBindings ? false
 , pythonBindings ? true
 , jdk ? null
+, ocaml ? null, findlib ? null, zarith ? null
 }:
 
 assert javaBindings -> jdk != null;
+assert ocamlBindings -> ocaml != null && findlib != null && zarith != null;
 
 with stdenv.lib;
 
@@ -19,13 +22,22 @@ stdenv.mkDerivation rec {
     sha256 = "1hnbzq10d23drd7ksm3c1n2611c3kd0q0yxgz8y78zaafwczvwxx";
   };
 
-  buildInputs = [ python fixDarwinDylibNames ] ++ optional javaBindings jdk;
+  buildInputs = [ python fixDarwinDylibNames ]
+  ++ optional javaBindings jdk
+  ++ optionals ocamlBindings [ ocaml findlib zarith ]
+  ;
   propagatedBuildInputs = [ python.pkgs.setuptools ];
   enableParallelBuilding = true;
 
+  postPatch = optionalString ocamlBindings ''
+    export OCAMLFIND_DESTDIR=$ocaml/lib/ocaml/${ocaml.version}/site-lib
+    mkdir -p $OCAMLFIND_DESTDIR/stublibs
+  '';
+
   configurePhase = concatStringsSep " " (
     [ "${python.interpreter} scripts/mk_make.py --prefix=$out" ]
     ++ optional javaBindings   "--java"
+    ++ optional ocamlBindings  "--ml"
     ++ optional pythonBindings "--python --pypkgdir=$out/${python.sitePackages}"
   ) + "\n" + "cd build";
 
@@ -39,7 +51,9 @@ stdenv.mkDerivation rec {
     ln -sf $lib/lib/libz3${stdenv.hostPlatform.extensions.sharedLibrary} $python/${python.sitePackages}/z3/lib/libz3${stdenv.hostPlatform.extensions.sharedLibrary}
   '';
 
-  outputs = [ "out" "lib" "dev" "python" ];
+  outputs = [ "out" "lib" "dev" "python" ]
+  ++ optional ocamlBindings "ocaml"
+  ;
 
   meta = {
     description = "A high-performance theorem prover and SMT solver";
diff --git a/pkgs/development/ocaml-modules/z3/default.nix b/pkgs/development/ocaml-modules/z3/default.nix
new file mode 100644
index 000000000000..d24a95102013
--- /dev/null
+++ b/pkgs/development/ocaml-modules/z3/default.nix
@@ -0,0 +1,29 @@
+{ stdenv, ocaml, findlib, zarith, z3 }:
+
+let z3-with-ocaml = z3.override {
+  ocamlBindings = true;
+  inherit ocaml findlib zarith;
+}; in
+
+stdenv.mkDerivation {
+
+  pname = "ocaml${ocaml.version}-z3";
+  inherit (z3-with-ocaml) version;
+
+  phases = [ "installPhase" "fixupPhase" ];
+
+  installPhase = ''
+    runHook preInstall
+    mkdir -p $OCAMLFIND_DESTDIR
+    cp -r ${z3-with-ocaml.ocaml}/lib/ocaml/${ocaml.version}/site-lib/stublibs $OCAMLFIND_DESTDIR
+    cp -r ${z3-with-ocaml.ocaml}/lib/ocaml/${ocaml.version}/site-lib/Z3 $OCAMLFIND_DESTDIR/z3
+    runHook postInstall
+  '';
+
+  buildInputs = [ findlib ];
+  propagatedBuildInputs = [ zarith ];
+
+  meta = z3.meta // {
+    description = "Z3 Theorem Prover (OCaml API)";
+  };
+}
diff --git a/pkgs/top-level/ocaml-packages.nix b/pkgs/top-level/ocaml-packages.nix
index ae1fe050b8ef..95c1bb300af5 100644
--- a/pkgs/top-level/ocaml-packages.nix
+++ b/pkgs/top-level/ocaml-packages.nix
@@ -993,6 +993,10 @@ let
 
     yojson = callPackage ../development/ocaml-modules/yojson { };
 
+    z3 = callPackage ../development/ocaml-modules/z3 {
+      inherit (pkgs) z3;
+    };
+
     zarith = callPackage ../development/ocaml-modules/zarith { };
 
     zed = callPackage ../development/ocaml-modules/zed { };