me/guix
Archived
1
0
Fork 0
Code Activity

gnu: z3: Build Python bindings.

Browse source 
* 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>
This commit is contained in:
Theodoros Foradis 2017-08-02 13:10:12 +03:00 • committed by Ludovic Courtès
parent bd2e321061
commit cf684d87d7
No known key found for this signature in database
GPG key ID: 090B11993D9AEBB5
1 changed files with 24 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

36
gnu/packages/maths.scm
View file

@ -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)
(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"))))
(add-before 'check 'make-test-z3
(lambda _
;; 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)))