GNU bug report logs - #27461
[PATCH] gnu: Add z3.

Previous Next

Full log

Message #38 received at 27461 <at> debbugs.gnu.org (full text, mbox):

From: Theodoros Foradis <theodoros.for <at> openmailbox.org>
To: 27461 <at> debbugs.gnu.org
Cc: dannym <at> scratchpost.org, ludo <at> gnu.org,
 Theodoros Foradis <theodoros.for <at> openmailbox.org>
Subject: [PATCH] gnu: Add python bindings to z3.
Date: Wed,  2 Aug 2017 13:10:12 +0300

* gnu/packages/maths.scm (z3): Add python bindings.
[build-system]: Change to cmake-build-system.
[arguments]<phases>: Remove "changedir" phase.
                     Add "bootstrap" phase.
[arguments]<configure-flags>: Add them.
[arguments]<tests>: Disable tests.
---
 gnu/packages/maths.scm | 27 +++++++++++++++------------
 1 file changed, 15 insertions(+), 12 deletions(-)

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 6566d750b..dfa06b852 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -3174,25 +3174,28 @@ as equations, scalars, vectors, and matrices.")
               (sha256
                (base32
                 "032a5lvji2liwmc25jv52bdrhimqflvqbpg77ccaq1jykhiivbmf"))))
-    (build-system gnu-build-system)
+    (build-system cmake-build-system)
     (arguments
-     `(#:test-target "test"
+     `(#:tests? #f ; no tests with cmake
+       #:configure-flags
+       (list "-DBUILD_PYTHON_BINDINGS=true"
+             "-DINSTALL_PYTHON_BINDINGS=true"
+             (string-append "-DCMAKE_INSTALL_PYTHON_PKG_DIR="
+                            %output
+                            "/lib/python2.7/site-packages")
+             (string-append "-DCMAKE_INSTALL_LIBDIR="
+                            %output
+                            "/lib"))
        #:phases
        (modify-phases %standard-phases
-         (replace 'configure
-           (lambda* (#:key inputs outputs #:allow-other-keys)
-             (zero?
-              (system* "python" "scripts/mk_make.py"
-                       (string-append "--prefix="
-                                      (assoc-ref outputs "out"))))))
-         (add-after 'configure 'change-dir
+         (add-before 'configure 'bootstrap
            (lambda _
-             (chdir "build")
-             #t)))))
+             (zero?
+              (system* "python" "contrib/cmake/bootstrap.py" "create")))))))
     (native-inputs
      `(("python" ,python-2)))
     (synopsis "Theorem prover")
     (description "Z3 is a theorem prover and @dfn{satisfiability modulo
-theories} (SMT) solver.  It provides a C/C++ API.")
+theories} (SMT) solver.  It provides a C/C++ API, as well as python bindings.")
     (home-page "https://github.com/Z3Prover/z3")
     (license license:expat)))
-- 
2.13.2

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.