(address . guix-patches@gnu.org)
20210205174641.166aec6f@tachikoma.lepiller.eu
Hi Guix!
This patch adds the OCaml bindings for the z3 package. I install it to
a separate output (but this only saves 3MB, maybe not that important).
I'm thinking we could build other bindings too, and it would be nice to
separate them also (after all, we probably don't need all of them at
the same time :)).
One issue is that this package installs the bindings to the Z3 ocaml
package. However, in opam, they override the install directory to be
z3, so we might have issues with dependents. Do you think I should also
override the name of the directory?
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(-)
Toggle diff (62 lines)
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