diff mbox series

[bug#46329] Add z3 OCaml bindings

Message ID 20210205174641.166aec6f@tachikoma.lepiller.eu
State Accepted
Headers show
Series [bug#46329] Add z3 OCaml bindings | expand

Checks

Context Check Description
cbaines/submitting builds success
cbaines/comparison success View comparision
cbaines/git branch success View Git branch
cbaines/applying patch fail View Laminar job
cbaines/issue success View issue

Commit Message

Julien Lepiller Feb. 5, 2021, 4:46 p.m. UTC 
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?

Comments

Ludovic Courtès March 19, 2021, 9:06 p.m. UTC | #1 
Hello!

Julien Lepiller <julien@lepiller.eu> skribis:

> 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 :)).

It’d be ideal if these could be built separately.  Like, we’d build z3,
and the ocaml-z3 package would depend on z3 (but use the same source
tarball as z3).

Does that seem feasible?

> 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?

I guess it depends on which one is the most widespread convention.

>>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.

I think a separate package as outline above would be slightly nicer, but
otherwise this patch LGTM.

Thanks,   :-)
Ludo’.
diff mbox series

Patch

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