diff options
| author | Theodoros Foradis <theodoros.for@openmailbox.org> | 2017-08-02 13:10:12 +0300 |
|---|---|---|
| committer | Ludovic Courtès <ludo@gnu.org> | 2017-08-21 17:04:53 +0200 |
| commit | cf684d87d7446ffe33ca4c73bf51dc24fa5a7129 (patch) | |
| tree | 6d583d433b24edf1ea93c42a0b10a616cb0c1382 | |
| parent | bd2e321061218729dec82fceba639aaee52bfff3 (diff) | |
| download | patches-cf684d87d7446ffe33ca4c73bf51dc24fa5a7129.tar patches-cf684d87d7446ffe33ca4c73bf51dc24fa5a7129.tar.gz | |
gnu: z3: Build Python bindings.
* 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 <ludo@gnu.org>
| -rw-r--r-- | gnu/packages/maths.scm | 34 |
1 files changed, 23 insertions, 11 deletions
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))) |