From 651701f64eaa81baf57634fc36efdab4d263e2b6 Mon Sep 17 00:00:00 2001 From: Julien Lepiller 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 ") "")) #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