From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from eggs.gnu.org ([2001:4830:134:3::10]:42221) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1dcqcO-0000Mk-2h for guix-patches@gnu.org; Wed, 02 Aug 2017 06:11:09 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1dcqcK-0004rH-4H for guix-patches@gnu.org; Wed, 02 Aug 2017 06:11:08 -0400 Received: from debbugs.gnu.org ([208.118.235.43]:35068) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1dcqcK-0004r0-0Z for guix-patches@gnu.org; Wed, 02 Aug 2017 06:11:04 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1dcqcH-0005nq-Qk for guix-patches@gnu.org; Wed, 02 Aug 2017 06:11:03 -0400 Subject: [bug#27461] [PATCH] gnu: Add python bindings to z3. Resent-Message-ID: From: Theodoros Foradis Date: Wed, 2 Aug 2017 13:10:12 +0300 Message-Id: <20170802101012.29210-1-theodoros.for@openmailbox.org> In-Reply-To: <87tw1q2sp7.fsf@openmailbox.org> References: <87tw1q2sp7.fsf@openmailbox.org> List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+kyle=kyleam.com@gnu.org Sender: "Guix-patches" To: 27461@debbugs.gnu.org * gnu/packages/maths.scm (z3): Add python bindings. [build-system]: Change to cmake-build-system. [arguments]: Remove "changedir" phase. Add "bootstrap" phase. [arguments]: Add them. [arguments]: 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