diff mbox series

[bug#46329,v2] Add z3 OCaml bindings

Message ID 20211008132618.2364711a@tachikoma.lepiller.eu
State Accepted
Headers show
Series [bug#46329,v2] Add z3 OCaml bindings | expand

Checks

Context Check Description
cbaines/comparison success View comparision
cbaines/git branch success View Git branch
cbaines/applying patch fail View Laminar job
cbaines/issue success View issue
cbaines/comparison success View comparision
cbaines/git branch success View Git branch
cbaines/applying patch fail View Laminar job
cbaines/issue success View issue
cbaines/comparison success View comparision
cbaines/git branch success View Git branch
cbaines/applying patch fail View Laminar job
cbaines/issue success View issue
cbaines/comparison success View comparision
cbaines/git branch success View Git branch
cbaines/applying patch fail View Laminar job
cbaines/issue success View issue
cbaines/comparison success View comparision
cbaines/git branch success View Git branch
cbaines/applying patch fail View Laminar job
cbaines/issue success View issue
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 Oct. 8, 2021, 11:26 a.m. UTC 
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.

Comments

Julien Lepiller Oct. 27, 2021, 10:27 p.m. UTC | #1 
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
diff mbox series

Patch

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