From: Julien Lepiller <julien@lepiller.eu>
To: 46329@debbugs.gnu.org
Subject: [bug#46329] [PATCH v2] Add z3 OCaml bindings
Date: Fri, 8 Oct 2021 13:26:18 +0200 [thread overview]
Message-ID: <20211008132618.2364711a@tachikoma.lepiller.eu> (raw)
In-Reply-To: <20210205174641.166aec6f@tachikoma.lepiller.eu>
[-- 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
next prev parent reply other threads:[~2021-10-08 11:27 UTC|newest]
Thread overview: 4+ messages / expand[flat|nested] mbox.gz Atom feed top
2021-02-05 16:46 [bug#46329] [PATCH] Add z3 OCaml bindings Julien Lepiller
2021-03-19 21:06 ` Ludovic Courtès
2021-10-08 11:26 ` Julien Lepiller [this message]
2021-10-27 22:27 ` bug#46329: [PATCH v2] " Julien Lepiller
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=20211008132618.2364711a@tachikoma.lepiller.eu \
--to=julien@lepiller.eu \
--cc=46329@debbugs.gnu.org \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
Code repositories for project(s) associated with this external index
https://git.savannah.gnu.org/cgit/guix.git
This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.