From 48aa690abd20a4e2134e4791eee388ca9f590ee9 Mon Sep 17 00:00:00 2001 From: Julien Lepiller 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