From cf684d87d7446ffe33ca4c73bf51dc24fa5a7129 Mon Sep 17 00:00:00 2001 From: Theodoros Foradis Date: Wed, 2 Aug 2017 13:10:12 +0300 Subject: gnu: z3: Build Python bindings. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * gnu/packages/maths.scm (z3): Add python bindings. [build-system]: Change to cmake-build-system. [arguments]: Remove "changedir" phase. Add "bootstrap" and "make-test-z3" phases; replace the "check" phase. Add #:configure-flags. Remove #:test-target. Signed-off-by: Ludovic Courtès --- gnu/packages/maths.scm | 34 +++++++++++++++++++++++----------- 1 file changed, 23 insertions(+), 11 deletions(-) (limited to 'gnu/packages') diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm index 3f1dc845fe..d1651e5a7b 100644 --- a/gnu/packages/maths.scm +++ b/gnu/packages/maths.scm @@ -3179,26 +3179,38 @@ as equations, scalars, vectors, and matrices.") (sha256 (base32 "032a5lvji2liwmc25jv52bdrhimqflvqbpg77ccaq1jykhiivbmf")))) - (build-system gnu-build-system) + (build-system cmake-build-system) (arguments - `(#:test-target "test" + `(#: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) + (add-before 'configure 'bootstrap + (lambda _ (zero? - (system* "python" "scripts/mk_make.py" - (string-append "--prefix=" - (assoc-ref outputs "out")))))) - (add-after 'configure 'change-dir + (system* "python" "contrib/cmake/bootstrap.py" "create")))) + (add-before 'check 'make-test-z3 (lambda _ - (chdir "build") - #t))))) + ;; Build the test suite executable. + (zero? (system* "make" "test-z3" "-j" + (number->string (parallel-job-count)))))) + (replace 'check + (lambda _ + ;; Run all the tests that don't require arguments. + (zero? (system* "./test-z3" "/a"))))))) (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))) -- cgit v1.2.3