[bug#46329] [PATCH] Add z3 OCaml bindings

[bug#46329] [PATCH] Add z3 OCaml bindings

[Julien Lepiller]

[-- Attachment #1: Type: text/plain, Size: 559 bytes --]

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?

[-- Attachment #2: 0001-gnu-z3-Build-and-install-OCaml-bindings.patch --]
[-- Type: text/x-patch, Size: 3304 bytes --]

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

[bug#46329] [PATCH] Add z3 OCaml bindings

[Ludovic Courtès]

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

[bug#46329] [PATCH v2] Add z3 OCaml bindings

[Julien Lepiller]

[-- Attachment #1: Type: text/plain, Size: 281 bytes --]

Hi!

I finally managed to build a separate package out of z3. It wasn't
easy, because the build system wants to rebuild a z3 and doesn't let
you install only the bindings. I managed to make it do just that: build
the bindings and install them, and link to the existing z3 package.

[-- Attachment #2: 0001-gnu-Add-ocaml-z3.patch --]
[-- Type: text/x-patch, Size: 3370 bytes --]

From 48aa690abd20a4e2134e4791eee388ca9f590ee9 Mon Sep 17 00:00:00 2001
From: Julien Lepiller <julien@lepiller.eu>
Date: Fri, 8 Oct 2021 13:23:37 +0200
Subject: [PATCH] gnu: Add ocaml-z3.

* gnu/packages/maths.scm (ocaml-z3): New variable.
---
 gnu/packages/maths.scm | 59 ++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 59 insertions(+)

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 038ca5518c..f87cdddfa8 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -5619,6 +5619,65 @@ as equations, scalars, vectors, and matrices.")
 theories} (SMT) solver.  It provides a C/C++ API, as well as Python bindings.")
     (license license:expat)))
 
+(define-public ocaml-z3
+  (package
+    (inherit z3)
+    (name "ocaml-z3")
+    (arguments
+     `(#:imported-modules ((guix build python-build-system)
+                           ,@%gnu-build-system-modules)
+       #:modules (((guix build python-build-system) #:select (site-packages))
+                  (guix build gnu-build-system)
+                  (guix build utils))
+       #:tests? #f; no ml tests
+       #:phases
+       (modify-phases %standard-phases
+         (add-before 'configure 'bootstrap
+           (lambda* (#:key outputs #:allow-other-keys)
+             (let ((out (assoc-ref outputs "out")))
+               (setenv "OCAMLFIND_LDCONF" "ignore")
+               (setenv "OCAMLFIND_DESTDIR" (string-append out "/lib/ocaml/site-lib"))
+               (mkdir-p (string-append out "/lib/ocaml/site-lib"))
+               (substitute* "scripts/mk_util.py"
+                 (("LIBZ3 = LIBZ3")
+                  (string-append "LIBZ3 = LIBZ3 + ' -dllpath " out "/lib'"))
+                 ;; Do not build z3 again, use the library passed as input
+                 ;; instead
+                 (("z3linkdep,") "\"\",")
+                 (("z3linkdep)") "\"\")"))
+               (invoke "python" "scripts/mk_make.py"))))
+         (replace 'configure
+           (lambda* (#:key inputs outputs #:allow-other-keys)
+             (invoke "./configure"
+                     "--ml"
+                     (string-append "--prefix=" (assoc-ref outputs "out")))))
+         (add-after 'configure 'change-directory
+           (lambda _
+             (chdir "build")
+             #t))
+         (replace 'build
+           (lambda _
+             (invoke "make" "ml")))
+         (replace 'install
+           (lambda* (#:key outputs #:allow-other-keys)
+             (invoke "ocamlfind" "install" "-destdir"
+                     (string-append (assoc-ref outputs "out") "/lib/ocaml/site-lib")
+                     "z3" "api/ml/META" "api/ml/z3enums.mli" "api/ml/z3enums.cmi"
+                     "api/ml/z3enums.cmx" "api/ml/z3native.mli"
+                     "api/ml/z3native.cmi" "api/ml/z3native.cmx"
+                     "../src/api/ml/z3.mli" "api/ml/z3.cmi" "api/ml/z3.cmx"
+                     "api/ml/libz3ml.a" "api/ml/z3ml.a" "api/ml/z3ml.cma"
+                     "api/ml/z3ml.cmxa" "api/ml/z3ml.cmxs" "api/ml/dllz3ml.so"))))))
+    (native-inputs
+     `(("which" ,which)
+       ("python" ,python-wrapper)
+       ("ocaml" ,ocaml)
+       ("ocaml-findlib" ,ocaml-findlib)))
+    (propagated-inputs
+     `(("ocaml-zarith" ,ocaml-zarith)))
+    (inputs
+     `(("z3" ,z3)))))
+
 (define-public elpa
   (package
     (name "elpa")
-- 
2.33.0

bug#46329: [PATCH v2] Add z3 OCaml bindings

[Julien Lepiller]

Le Fri, 8 Oct 2021 13:26:18 +0200,
Julien Lepiller <julien@lepiller.eu> a écrit :

> Hi!
> 
> I finally managed to build a separate package out of z3. It wasn't
> easy, because the build system wants to rebuild a z3 and doesn't let
> you install only the bindings. I managed to make it do just that:
> build the bindings and install them, and link to the existing z3
> package.

After more than two weeks of silence, pushed to master as
a8c69e22ee2f9e7b487ffe0b567297f28863128d