>From 651701f64eaa81baf57634fc36efdab4d263e2b6 Mon Sep 17 00:00:00 2001
From: Julien Lepiller <julien@lepiller.eu>
Date: Tue, 2 Feb 2021 22:17:19 +0100
Subject: [PATCH] gnu: z3: Build and install OCaml bindings.

* gnu/packages/maths.scm (z3)[outputs]: Add ocaml output.
[arguments]: Build and install OCaml bindings.
---
 gnu/packages/maths.scm | 21 ++++++++++++++++++---
 1 file changed, 18 insertions(+), 3 deletions(-)

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index eff1480e62..2797bc8ae4 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -116,6 +116,7 @@
   #:use-module (gnu packages mpi)
   #:use-module (gnu packages multiprecision)
   #:use-module (gnu packages netpbm)
+  #:use-module (gnu packages ocaml)
   #:use-module (gnu packages onc-rpc)
   #:use-module (gnu packages pcre)
   #:use-module (gnu packages popt)
@@ -4741,6 +4742,7 @@ as equations, scalars, vectors, and matrices.")
                (base32
                 "1hnbzq10d23drd7ksm3c1n2611c3kd0q0yxgz8y78zaafwczvwxx"))))
     (build-system gnu-build-system)
+    (outputs '("out" "ocaml"))
     (arguments
      `(#:imported-modules ((guix build python-build-system)
                            ,@%gnu-build-system-modules)
@@ -4760,8 +4762,16 @@ as equations, scalars, vectors, and matrices.")
                (("#include <immintrin.h>") ""))
              #t))
          (add-before 'configure 'bootstrap
-           (lambda _
-             (invoke "python" "scripts/mk_make.py")))
+           (lambda* (#:key outputs #:allow-other-keys)
+             (let ((ocaml (assoc-ref outputs "ocaml"))
+                   (out (assoc-ref outputs "out")))
+               (setenv "OCAMLFIND_LDCONF" "ignore")
+               (setenv "OCAMLFIND_DESTDIR" (string-append ocaml "/lib/ocaml/site-lib"))
+               (mkdir-p (string-append ocaml "/lib/ocaml/site-lib"))
+               (substitute* "scripts/mk_util.py"
+                 (("LIBZ3 = LIBZ3")
+                  (string-append "LIBZ3 = LIBZ3 + ' -dllpath " out "/lib'")))
+               (invoke "python" "scripts/mk_make.py"))))
          ;; work around gnu-build-system's setting --enable-fast-install
          ;; (z3's `configure' is a wrapper around the above python file,
          ;; which fails when passed --enable-fast-install)
@@ -4769,6 +4779,7 @@ as equations, scalars, vectors, and matrices.")
            (lambda* (#:key inputs outputs #:allow-other-keys)
              (invoke "./configure"
                      "--python"
+                     "--ml"
                      (string-append "--prefix=" (assoc-ref outputs "out"))
                      (string-append "--pypkgdir=" (site-packages inputs outputs)))))
          (add-after 'configure 'change-directory
@@ -4786,7 +4797,11 @@ as equations, scalars, vectors, and matrices.")
              (invoke "./test-z3" "/a"))))))
     (native-inputs
      `(("which" ,which)
-       ("python" ,python-wrapper)))
+       ("python" ,python-wrapper)
+       ("ocaml" ,ocaml)
+       ("ocaml-findlib" ,ocaml-findlib)))
+    (inputs
+     `(("ocaml-zarith" ,ocaml-zarith)))
     (synopsis "Theorem prover")
     (description "Z3 is a theorem prover and @dfn{satisfiability modulo
 theories} (SMT) solver.  It provides a C/C++ API, as well as Python bindings.")
-- 
2.30.0