From unknown Mon Jun 23 16:45:08 2025 Content-Disposition: inline Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 X-Mailer: MIME-tools 5.509 (Entity 5.509) Content-Type: text/plain; charset=utf-8 From: bug#27461 <27461@debbugs.gnu.org> To: bug#27461 <27461@debbugs.gnu.org> Subject: Status: [PATCH] gnu: Add z3. Reply-To: bug#27461 <27461@debbugs.gnu.org> Date: Mon, 23 Jun 2025 23:45:08 +0000 retitle 27461 [PATCH] gnu: Add z3. reassign 27461 guix-patches submitter 27461 Theodoros Foradis severity 27461 normal tag 27461 patch thanks From debbugs-submit-bounces@debbugs.gnu.org Fri Jun 23 11:51:03 2017 Received: (at submit) by debbugs.gnu.org; 23 Jun 2017 15:51:03 +0000 Received: from localhost ([127.0.0.1]:34659 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dOQrG-0004NF-KQ for submit@debbugs.gnu.org; Fri, 23 Jun 2017 11:51:02 -0400 Received: from eggs.gnu.org ([208.118.235.92]:57608) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dOQrE-0004N2-RP for submit@debbugs.gnu.org; Fri, 23 Jun 2017 11:50:53 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1dOQr7-0001ZJ-Uo for submit@debbugs.gnu.org; Fri, 23 Jun 2017 11:50:47 -0400 X-Spam-Checker-Version: SpamAssassin 3.3.2 (2011-06-06) on eggs.gnu.org X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=BAYES_40,T_DKIM_INVALID autolearn=disabled version=3.3.2 Received: from lists.gnu.org ([2001:4830:134:3::11]:39596) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1dOQr7-0001Z9-Q7 for submit@debbugs.gnu.org; Fri, 23 Jun 2017 11:50:45 -0400 Received: from eggs.gnu.org ([2001:4830:134:3::10]:48572) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1dOQr6-00071x-8x for guix-patches@gnu.org; Fri, 23 Jun 2017 11:50:45 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1dOQr2-0001XN-M9 for guix-patches@gnu.org; Fri, 23 Jun 2017 11:50:44 -0400 Received: from lb1.openmailbox.org ([5.79.108.160]:33494 helo=mail.openmailbox.org) by eggs.gnu.org with esmtps (TLS1.0:DHE_RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1dOQr2-0001WL-84 for guix-patches@gnu.org; Fri, 23 Jun 2017 11:50:40 -0400 Received: by mail.openmailbox.org (Postfix, from userid 20002) id 0F4B3540CCB; Fri, 23 Jun 2017 17:50:35 +0200 (CEST) DKIM-Signature: v=1; a=rsa-sha256; c=simple/simple; d=openmailbox.org; s=openmailbox; t=1498233037; bh=FNIR1SgJ+wtzR7zXdf7bVyW+6Tp42M9TrG9OWQdTbBs=; h=From:To:Cc:Subject:Date:From; b=w5kEpE/IJC768TSQyCzCCyq6cDcPq50jloLnzasMROIX48JJMaZ43YB9btJVD0oDW 0az7Wy0BwiPW+c8EyW856QhFsoTibiQ0ncSss7pMvbRxgJREr9VPrRQwG7O8fAZhvL ZMbEw35qqlyzEXQ0FCKdQHqJzlSugHF63wAaZKJ4= From: Theodoros Foradis DKIM-Signature: v=1; a=rsa-sha256; c=simple/simple; d=openmailbox.org; s=openmailbox; t=1498233034; bh=FNIR1SgJ+wtzR7zXdf7bVyW+6Tp42M9TrG9OWQdTbBs=; h=From:To:Cc:Subject:Date:From; b=L0/rNtP5kHqklaoHQ207g10c/NYIySeUg9OCbuioc+A/m+sLq7tqXzgx0NX4eoyAg z+OukbVnSAdKbEfkVz1NI/+0pcAVw8+uEM33jEqHgMDfvd9YsqXLrC0tsQI61NxfCX owT3p8G4eVt3KOR08QAuYfbQI8r4PBYp9asB8FAg= To: guix-patches@gnu.org Subject: [PATCH] gnu: Add z3. Date: Fri, 23 Jun 2017 18:50:22 +0300 Message-Id: <20170623155022.16252-1-theodoros.for@openmailbox.org> X-Mailer: git-send-email 2.13.1 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] [fuzzy] X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.6.x X-Received-From: 2001:4830:134:3::11 X-Spam-Score: -4.0 (----) X-Debbugs-Envelope-To: submit Cc: Theodoros Foradis X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: 1.0 (+) * gnu/packages/maths.scm (z3): New variable. * gnu/packages/fpga.scm (yosys): Add z3 to propagated-inputs. --- gnu/packages/fpga.scm | 5 ++++- gnu/packages/maths.scm | 34 ++++++++++++++++++++++++++++++++++ 2 files changed, 38 insertions(+), 1 deletion(-) diff --git a/gnu/packages/fpga.scm b/gnu/packages/fpga.scm index 420d0aff2..220877577 100644 --- a/gnu/packages/fpga.scm +++ b/gnu/packages/fpga.scm @@ -1,6 +1,6 @@ ;;; GNU Guix --- Functional package management for GNU ;;; Copyright =C2=A9 2016 Danny Milosavljevic -;;; Copyright =C2=A9 2016 Theodoros Foradis +;;; Copyright =C2=A9 2016, 2017 Theodoros Foradis ;;; ;;; This file is part of GNU Guix. ;;; @@ -36,6 +36,7 @@ #:use-module (gnu packages graphviz) #:use-module (gnu packages libffi) #:use-module (gnu packages linux) + #:use-module (gnu packages maths) #:use-module (gnu packages perl) #:use-module (gnu packages ghostscript) #:use-module (gnu packages gperf) @@ -198,6 +199,8 @@ For synthesis, the compiler generates netlists in the= desired format.") ("psmisc" ,psmisc) ("xdot" ,xdot) ("abc" ,abc))) + (propagated-inputs + `(("z3" ,z3))) ; should be in path for yosys-smtbmc (home-page "http://www.clifford.at/yosys/") (synopsis "FPGA Verilog RTL synthesizer") (description "Yosys synthesizes Verilog-2005.") diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm index 1115cef59..3ee0beeef 100644 --- a/gnu/packages/maths.scm +++ b/gnu/packages/maths.scm @@ -18,6 +18,7 @@ ;;; Copyright =C2=A9 2017 Paul Garlick ;;; Copyright =C2=A9 2017 ng0 ;;; Copyright =C2=A9 2017 Ben Woodcroft +;;; Copyright =C2=A9 2017 Theodoros Foradis ;;; ;;; This file is part of GNU Guix. ;;; @@ -3129,3 +3130,36 @@ as equations, scalars, vectors, and matrices.") (home-page "https://www.gnu.org/software/jacal/") (license license:gpl3+))) =20 +(define-public z3 + (package + (name "z3") + (version "4.5.0") + (source (origin + (method url-fetch) + (uri (string-append + "https://github.com/Z3Prover/z3/archive/z3-" + version ".tar.gz")) + (sha256 + (base32 + "032a5lvji2liwmc25jv52bdrhimqflvqbpg77ccaq1jykhiivbmf"))= )) + (build-system gnu-build-system) + (arguments + `(#:test-target "test" + #:phases + (modify-phases %standard-phases + (replace 'configure + (lambda* (#:key inputs outputs #:allow-other-keys) + (zero? + (system* "python" "scripts/mk_make.py" + (string-append "--prefix=3D" + (assoc-ref outputs "out")))))) + (add-after 'configure 'change-dir + (lambda _ + (chdir "build") + #t))))) + (native-inputs + `(("python" ,python-2))) + (synopsis "Theorem prover") + (description "@code{z3} is a theorem prover.") + (home-page "https://github.com/Z3Prover/z3") + (license license:expat) )) --=20 2.13.1 From debbugs-submit-bounces@debbugs.gnu.org Sun Jun 25 04:20:11 2017 Received: (at 27461) by debbugs.gnu.org; 25 Jun 2017 08:20:11 +0000 Received: from localhost ([127.0.0.1]:36275 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dP2m1-00051O-OQ for submit@debbugs.gnu.org; Sun, 25 Jun 2017 04:20:11 -0400 Received: from 89-92-10-219.hfc.dyn.abo.bbox.fr ([89.92.10.219]:36626 helo=skaro.lepiller.eu) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dP2ly-00050z-R1 for 27461@debbugs.gnu.org; Sun, 25 Jun 2017 04:19:59 -0400 Received: from localhost (localhost [127.0.0.1]) by skaro.lepiller.eu (Postfix) with ESMTP id 3933D80B36 for <27461@debbugs.gnu.org>; Sun, 25 Jun 2017 10:19:52 +0200 (CEST) X-Virus-Scanned: Debian amavisd-new at lepiller.eu Received: from skaro.lepiller.eu ([127.0.0.1]) by localhost (lepiller.eu [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id oTPshQwG-tie for <27461@debbugs.gnu.org>; Sun, 25 Jun 2017 10:19:45 +0200 (CEST) Received: from webmail.lepiller.eu (localhost [127.0.0.1]) by skaro.lepiller.eu (Postfix) with ESMTPA id DF7808073F for <27461@debbugs.gnu.org>; Sun, 25 Jun 2017 10:19:44 +0200 (CEST) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 8bit Date: Sun, 25 Jun 2017 10:19:44 +0200 From: julien lepiller To: 27461@debbugs.gnu.org Subject: Re: [bug#27461] [PATCH] gnu: Add z3. In-Reply-To: <20170623155022.16252-1-theodoros.for@openmailbox.org> References: <20170623155022.16252-1-theodoros.for@openmailbox.org> Message-ID: <85aa5980dfa7244056fdd3726cc60ad1@lepiller.eu> X-Sender: julien@lepiller.eu User-Agent: Roundcube Webmail/1.2.5 X-Spam-Score: 3.9 (+++) X-Spam-Report: Spam detection software, running on the system "debbugs.gnu.org", has NOT identified this incoming email as spam. The original message has been attached to this so you can view it or label similar future email. If you have any questions, see the administrator of that system for details. Content preview: Hi, I don't have a patch for this yet, but I was working on z3 as a dependency of angr. So here is what I got. As you can see, I separated the package in two: the library itself, and the python module that uses that library. I'm doing this because there are other languages than python. What do you think? [...] Content analysis details: (3.9 points, 10.0 required) pts rule name description ---- ---------------------- -------------------------------------------------- 3.6 RCVD_IN_PBL RBL: Received via a relay in Spamhaus PBL [89.92.10.219 listed in zen.spamhaus.org] 0.0 TVD_RCVD_IP Message was received from an IP address 0.4 RDNS_DYNAMIC Delivered to internal network by host with dynamic-looking rDNS X-Debbugs-Envelope-To: 27461 X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: 0.4 (/) Hi, I don't have a patch for this yet, but I was working on z3 as a dependency of angr. So here is what I got. As you can see, I separated the package in two: the library itself, and the python module that uses that library. I'm doing this because there are other languages than python. What do you think? (define-public z3-solver (package (name "z3-solver") (version "4.5.0") (source (origin (method url-fetch) (uri (string-append "https://github.com/Z3Prover/z3/archive/z3-" version ".tar.gz")) (sha256 (base32 "032a5lvji2liwmc25jv52bdrhimqflvqbpg77ccaq1jykhiivbmf")) (file-name (string-append name "-" version ".tar.gz")))) (build-system gnu-build-system) (arguments `(#:phases (modify-phases %standard-phases (delete 'configure) (add-before 'build 'generate-make (lambda _ (system* "python" "scripts/mk_make.py") (chdir "build")))) #:test-target "test" #:make-flags (list (string-append "PREFIX=" (assoc-ref %outputs "out"))))) (native-inputs `(("python" ,python-2))) (home-page "https://github.com/Z3Prover/z3") (synopsis "SMT solver library") (description "Z3 is a theorem prover from Microsoft Research.") (license license:expat))) (define-public python2-z3-solver (package (inherit z3-solver) (name "python2-z3-solver") (build-system python-build-system) (propagated-inputs `(("z3" ,z3-solver))) (arguments `(#:python ,python-2 #:phases (modify-phases %standard-phases (add-before 'build 'prepare (lambda* (#:key inputs #:allow-other-keys) (system* "python" "scripts/mk_make.py") (copy-file "build/python/z3/z3core.py" "src/api/python/z3/z3core.py") (copy-file "build/python/z3/z3consts.py" "src/api/python/z3/z3consts.py") (chdir "src/api/python") (substitute* "z3/z3core.py" (("_dirs = \\[") (string-append "_dirs = ['" (assoc-ref inputs "z3") "/lib', "))) (substitute* "MANIFEST.in" ((".*") "")) (substitute* "setup.py" (("self.execute\\(.*") "\n") (("scripts=.*") "\n"))))))))) Le 2017-06-23 17:50, Theodoros Foradis a écrit : > * gnu/packages/maths.scm (z3): New variable. > * gnu/packages/fpga.scm (yosys): Add z3 to propagated-inputs. > --- > gnu/packages/fpga.scm | 5 ++++- > gnu/packages/maths.scm | 34 ++++++++++++++++++++++++++++++++++ > 2 files changed, 38 insertions(+), 1 deletion(-) > > diff --git a/gnu/packages/fpga.scm b/gnu/packages/fpga.scm > index 420d0aff2..220877577 100644 > --- a/gnu/packages/fpga.scm > +++ b/gnu/packages/fpga.scm > @@ -1,6 +1,6 @@ > ;;; GNU Guix --- Functional package management for GNU > ;;; Copyright © 2016 Danny Milosavljevic > -;;; Copyright © 2016 Theodoros Foradis > +;;; Copyright © 2016, 2017 Theodoros Foradis > > ;;; > ;;; This file is part of GNU Guix. > ;;; > @@ -36,6 +36,7 @@ > #:use-module (gnu packages graphviz) > #:use-module (gnu packages libffi) > #:use-module (gnu packages linux) > + #:use-module (gnu packages maths) > #:use-module (gnu packages perl) > #:use-module (gnu packages ghostscript) > #:use-module (gnu packages gperf) > @@ -198,6 +199,8 @@ For synthesis, the compiler generates netlists in > the desired format.") > ("psmisc" ,psmisc) > ("xdot" ,xdot) > ("abc" ,abc))) > + (propagated-inputs > + `(("z3" ,z3))) ; should be in path for yosys-smtbmc > (home-page "http://www.clifford.at/yosys/") > (synopsis "FPGA Verilog RTL synthesizer") > (description "Yosys synthesizes Verilog-2005.") > diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm > index 1115cef59..3ee0beeef 100644 > --- a/gnu/packages/maths.scm > +++ b/gnu/packages/maths.scm > @@ -18,6 +18,7 @@ > ;;; Copyright © 2017 Paul Garlick > > ;;; Copyright © 2017 ng0 > ;;; Copyright © 2017 Ben Woodcroft > +;;; Copyright © 2017 Theodoros Foradis > ;;; > ;;; This file is part of GNU Guix. > ;;; > @@ -3129,3 +3130,36 @@ as equations, scalars, vectors, and matrices.") > (home-page "https://www.gnu.org/software/jacal/") > (license license:gpl3+))) > > +(define-public z3 > + (package > + (name "z3") > + (version "4.5.0") > + (source (origin > + (method url-fetch) > + (uri (string-append > + "https://github.com/Z3Prover/z3/archive/z3-" > + version ".tar.gz")) > + (sha256 > + (base32 > + > "032a5lvji2liwmc25jv52bdrhimqflvqbpg77ccaq1jykhiivbmf")))) > + (build-system gnu-build-system) > + (arguments > + `(#:test-target "test" > + #: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 > + (lambda _ > + (chdir "build") > + #t))))) > + (native-inputs > + `(("python" ,python-2))) > + (synopsis "Theorem prover") > + (description "@code{z3} is a theorem prover.") > + (home-page "https://github.com/Z3Prover/z3") > + (license license:expat) )) From debbugs-submit-bounces@debbugs.gnu.org Mon Jun 26 13:14:17 2017 Received: (at 27461) by debbugs.gnu.org; 26 Jun 2017 17:14:17 +0000 Received: from localhost ([127.0.0.1]:39359 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dPXaW-0003OV-Fu for submit@debbugs.gnu.org; Mon, 26 Jun 2017 13:14:17 -0400 Received: from lb1.openmailbox.org ([5.79.108.160]:49138 helo=mail.openmailbox.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dPXaU-0003OM-T5 for 27461@debbugs.gnu.org; Mon, 26 Jun 2017 13:14:11 -0400 Received: by mail.openmailbox.org (Postfix, from userid 20002) id 12A0B506B74; Mon, 26 Jun 2017 18:31:34 +0200 (CEST) DKIM-Signature: v=1; a=rsa-sha256; c=simple/simple; d=openmailbox.org; s=openmailbox; t=1498497249; bh=Cp4BCk870dxVvKXHiUVNNWsljY4Vt5qyC9ytUSdIgWU=; h=References:From:To:Cc:Subject:In-reply-to:Date:From; b=RIzX1EfBoCKC0L/myzRRZJC5GCt2YG900vtJVMRINoXGa20iAJijOFpqFN9rLf9bd pHAcVlHo0iOeUv7nv1CF+Wg8EP6wrdJJCGE4spDBOp/L1SkJZ5xX3pPabEZlVHj0Ec +fmEbkDre4ZW9zcFl3pYEkAyVJgJ5F1Wpcsm3C6g= X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on ZDZR003 X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=NO_RECEIVED,NO_RELAYS, T_DKIM_INVALID,URIBL_BLOCKED autolearn=disabled version=3.4.0 References: <20170623155022.16252-1-theodoros.for@openmailbox.org> <85aa5980dfa7244056fdd3726cc60ad1@lepiller.eu> DKIM-Signature: v=1; a=rsa-sha256; c=simple/simple; d=openmailbox.org; s=openmailbox; t=1498494693; bh=Cp4BCk870dxVvKXHiUVNNWsljY4Vt5qyC9ytUSdIgWU=; h=References:From:To:Cc:Subject:In-reply-to:Date:From; b=rY3sWa0ANwQPYQ4iLrRDr/cf73HjHgPesa5DnJ6+zE3XOq+/OUu0uK+dhYdKuBpuz pcJFkfWdVEqkHGeG8z0fVrDkmGuG7umyW31X1v872/GmvQoPuIQ7AUvmzx2hsGGhMZ nM/uBb/PezhYZu+ZgCbGiXS/QNRdl+JuPjEmNGOs= User-agent: mu4e 0.9.18; emacs 25.2.1 From: Theodoros Foradis To: julien lepiller Subject: Re: [bug#27461] [PATCH] gnu: Add z3. Message-ID: <87efu6r9s6.fsf@openmailbox.org> In-reply-to: <85aa5980dfa7244056fdd3726cc60ad1@lepiller.eu> Date: Mon, 26 Jun 2017 19:31:15 +0300 MIME-Version: 1.0 Content-Type: text/plain X-Spam-Score: -0.2 (/) X-Debbugs-Envelope-To: 27461 Cc: Theodoros Foradis , 27461@debbugs.gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: 0.5 (/) Hello, > Hi, > > I don't have a patch for this yet, but I was working on z3 as a > dependency of angr. So here is what I got. > > As you can see, I separated the package in two: the library itself, and > the python module that uses that library. I'm doing this because there > are other languages than python. What do you think? > > (define-public z3-solver > (package > (name "z3-solver") > (version "4.5.0") > (source (origin > (method url-fetch) > (uri (string-append > "https://github.com/Z3Prover/z3/archive/z3-" > version ".tar.gz")) > (sha256 > (base32 > "032a5lvji2liwmc25jv52bdrhimqflvqbpg77ccaq1jykhiivbmf")) > (file-name (string-append name "-" version ".tar.gz")))) > (build-system gnu-build-system) > (arguments > `(#:phases > (modify-phases %standard-phases > (delete 'configure) > (add-before 'build 'generate-make > (lambda _ > (system* "python" "scripts/mk_make.py") > (chdir "build")))) > #:test-target "test" > #:make-flags > (list (string-append "PREFIX=" (assoc-ref %outputs "out"))))) > (native-inputs > `(("python" ,python-2))) > (home-page "https://github.com/Z3Prover/z3") > (synopsis "SMT solver library") > (description "Z3 is a theorem prover from Microsoft Research.") > (license license:expat))) > This is very similar to my package. The minor difference is that I only pass the prefix once during configure (running the "scripts/mk_make.py), instead of both incovations of make. Also, if it's more correct, I can merge the 2 phases (configure and change-dir) into one, as you do. > (define-public python2-z3-solver > (package > (inherit z3-solver) > (name "python2-z3-solver") > (build-system python-build-system) > (propagated-inputs > `(("z3" ,z3-solver))) > (arguments > `(#:python ,python-2 > #:phases > (modify-phases %standard-phases > (add-before 'build 'prepare > (lambda* (#:key inputs #:allow-other-keys) > (system* "python" "scripts/mk_make.py") > (copy-file "build/python/z3/z3core.py" > "src/api/python/z3/z3core.py") > (copy-file "build/python/z3/z3consts.py" > "src/api/python/z3/z3consts.py") > (chdir "src/api/python") > (substitute* "z3/z3core.py" > (("_dirs = \\[") > (string-append "_dirs = ['" (assoc-ref inputs "z3") > "/lib', "))) > (substitute* "MANIFEST.in" > ((".*") "")) > (substitute* "setup.py" > (("self.execute\\(.*") "\n") > (("scripts=.*") "\n"))))))))) This builds correctly for me, though I'm no expert in python packaging. Since this will likely be in a different file (python.scm?), maybe we can proceed with just z3 if others are ok with it, and then you only add python2-z3 later, in the patch-set with angr? Or maybe it would be preferable to have just one z3 package also providing the python bindings? I think seperate packages are better, though. Regards, -- Theodoros Foradis From debbugs-submit-bounces@debbugs.gnu.org Thu Jul 20 05:22:55 2017 Received: (at 27461) by debbugs.gnu.org; 20 Jul 2017 09:22:55 +0000 Received: from localhost ([127.0.0.1]:48587 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dY7fb-0000dG-A5 for submit@debbugs.gnu.org; Thu, 20 Jul 2017 05:22:55 -0400 Received: from eggs.gnu.org ([208.118.235.92]:59679) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dY7fa-0000d1-8V for 27461@debbugs.gnu.org; Thu, 20 Jul 2017 05:22:54 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1dY7fS-00067n-35 for 27461@debbugs.gnu.org; Thu, 20 Jul 2017 05:22:49 -0400 X-Spam-Checker-Version: SpamAssassin 3.3.2 (2011-06-06) on eggs.gnu.org X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,RP_MATCHES_RCVD autolearn=disabled version=3.3.2 Received: from fencepost.gnu.org ([2001:4830:134:3::e]:54766) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1dY7fR-00067h-Vh; Thu, 20 Jul 2017 05:22:46 -0400 Received: from [193.50.110.220] (port=39474 helo=ribbon) by fencepost.gnu.org with esmtpsa (TLS1.2:RSA_AES_256_CBC_SHA1:256) (Exim 4.82) (envelope-from ) id 1dY7fR-0003ng-Gf; Thu, 20 Jul 2017 05:22:45 -0400 From: ludo@gnu.org (Ludovic =?utf-8?Q?Court=C3=A8s?=) To: Theodoros Foradis Subject: Re: [bug#27461] [PATCH] gnu: Add z3. References: <20170623155022.16252-1-theodoros.for@openmailbox.org> <85aa5980dfa7244056fdd3726cc60ad1@lepiller.eu> <87efu6r9s6.fsf@openmailbox.org> Date: Thu, 20 Jul 2017 11:22:43 +0200 In-Reply-To: <87efu6r9s6.fsf@openmailbox.org> (Theodoros Foradis's message of "Mon, 26 Jun 2017 19:31:15 +0300") Message-ID: <8760enxy1o.fsf@gnu.org> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/25.2 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Received-From: 2001:4830:134:3::e X-Spam-Score: -5.0 (-----) X-Debbugs-Envelope-To: 27461 Cc: julien lepiller , 27461@debbugs.gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -5.0 (-----) Hello, Theodoros, Julien: could one of you submit an updated patch/patch set that incorporates what both of you did? If there are still fine points to discuss, that can always happen at a later stage. Thanks, Ludo=E2=80=99. From debbugs-submit-bounces@debbugs.gnu.org Tue Jul 25 12:11:35 2017 Received: (at 27461) by debbugs.gnu.org; 25 Jul 2017 16:11:35 +0000 Received: from localhost ([127.0.0.1]:56152 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1da2Qi-0001sx-Ji for submit@debbugs.gnu.org; Tue, 25 Jul 2017 12:11:35 -0400 Received: from lb1.openmailbox.org ([5.79.108.160]:52616 helo=mail.openmailbox.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1da2Qg-0001so-6C for 27461@debbugs.gnu.org; Tue, 25 Jul 2017 12:11:27 -0400 Received: by mail.openmailbox.org (Postfix, from userid 20002) id 813BD4E3E49; Tue, 25 Jul 2017 18:11:24 +0200 (CEST) DKIM-Signature: v=1; a=rsa-sha256; c=simple/simple; d=openmailbox.org; s=openmailbox; t=1500999085; bh=oxtgKkyhpdXKY7I9uLmm5WMsqFWE2pUBwnBnQaNjvjA=; h=From:To:Cc:Subject:Date:In-Reply-To:References:From; b=eDr8SUDfir2jRUBj14KJ2QeAh/zuOTb1i4ps2gd5SVPlLrDaFf5/m+WTQSQ1TjrIp 1sKStsuIDw+U9XBNsXa5qNvPNQkew80LJchoiQrY+RXkyZksFpb+p+2FtKMk7YFhEu T7CJNX7u0PozzxFS7t3696l4ElSjj0G0MlrtGZls= X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on ZDZR003 X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=NO_RECEIVED,NO_RELAYS, T_DKIM_INVALID autolearn=disabled version=3.4.0 From: Theodoros Foradis DKIM-Signature: v=1; a=rsa-sha256; c=simple/simple; d=openmailbox.org; s=openmailbox; t=1500999084; bh=oxtgKkyhpdXKY7I9uLmm5WMsqFWE2pUBwnBnQaNjvjA=; h=From:To:Cc:Subject:Date:In-Reply-To:References:From; b=fmoFUtKis/WW1qYOj2P47Xq7foXrw1Ji1E09PpLAo7uwjTgYfY4gOoCJyO2MjSgfh dOeV8CgJbM3AgGeN/n0i82VxeUaXi9yRmpqyrOvidMSQlMoh+VzbQPWTmMXiLc5e97 phPO0HR3BikKtwK6gtexOHRxqVXjcY7fhQljeevY= To: 27461@debbugs.gnu.org Subject: [PATCH v2 1/2] gnu: Add z3. Date: Tue, 25 Jul 2017 19:11:12 +0300 Message-Id: <20170725161113.26165-1-theodoros.for@openmailbox.org> X-Mailer: git-send-email 2.13.2 In-Reply-To: <8760enxy1o.fsf@gnu.org> References: <8760enxy1o.fsf@gnu.org> MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit X-Spam-Score: 0.5 (/) X-Debbugs-Envelope-To: 27461 Cc: ludo@gnu.org, julien@lepiller.eu, Theodoros Foradis X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: 0.0 (/) * gnu/packages/maths.scm (z3): New variable. * gnu/packages/fpga.scm (yosys): Add z3 to propagated-inputs. --- gnu/packages/fpga.scm | 5 ++++- gnu/packages/maths.scm | 34 ++++++++++++++++++++++++++++++++++ 2 files changed, 38 insertions(+), 1 deletion(-) diff --git a/gnu/packages/fpga.scm b/gnu/packages/fpga.scm index 420d0aff2..220877577 100644 --- a/gnu/packages/fpga.scm +++ b/gnu/packages/fpga.scm @@ -1,6 +1,6 @@ ;;; GNU Guix --- Functional package management for GNU ;;; Copyright © 2016 Danny Milosavljevic -;;; Copyright © 2016 Theodoros Foradis +;;; Copyright © 2016, 2017 Theodoros Foradis ;;; ;;; This file is part of GNU Guix. ;;; @@ -36,6 +36,7 @@ #:use-module (gnu packages graphviz) #:use-module (gnu packages libffi) #:use-module (gnu packages linux) + #:use-module (gnu packages maths) #:use-module (gnu packages perl) #:use-module (gnu packages ghostscript) #:use-module (gnu packages gperf) @@ -198,6 +199,8 @@ For synthesis, the compiler generates netlists in the desired format.") ("psmisc" ,psmisc) ("xdot" ,xdot) ("abc" ,abc))) + (propagated-inputs + `(("z3" ,z3))) ; should be in path for yosys-smtbmc (home-page "http://www.clifford.at/yosys/") (synopsis "FPGA Verilog RTL synthesizer") (description "Yosys synthesizes Verilog-2005.") diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm index 5e4cd8586..536fb9bed 100644 --- a/gnu/packages/maths.scm +++ b/gnu/packages/maths.scm @@ -18,6 +18,7 @@ ;;; Copyright © 2017 Paul Garlick ;;; Copyright © 2017 ng0 ;;; Copyright © 2017 Ben Woodcroft +;;; Copyright © 2017 Theodoros Foradis ;;; ;;; This file is part of GNU Guix. ;;; @@ -3141,3 +3142,36 @@ as equations, scalars, vectors, and matrices.") (home-page "https://www.gnu.org/software/jacal/") (license license:gpl3+))) +(define-public z3 + (package + (name "z3") + (version "4.5.0") + (source (origin + (method url-fetch) + (uri (string-append + "https://github.com/Z3Prover/z3/archive/z3-" + version ".tar.gz")) + (sha256 + (base32 + "032a5lvji2liwmc25jv52bdrhimqflvqbpg77ccaq1jykhiivbmf")))) + (build-system gnu-build-system) + (arguments + `(#:test-target "test" + #: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 + (lambda _ + (chdir "build") + #t))))) + (native-inputs + `(("python" ,python-2))) + (synopsis "Theorem prover") + (description "@code{z3} is a theorem prover.") + (home-page "https://github.com/Z3Prover/z3") + (license license:expat))) -- 2.13.2 From debbugs-submit-bounces@debbugs.gnu.org Tue Jul 25 12:11:39 2017 Received: (at 27461) by debbugs.gnu.org; 25 Jul 2017 16:11:39 +0000 Received: from localhost ([127.0.0.1]:56155 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1da2Qq-0001tJ-CP for submit@debbugs.gnu.org; Tue, 25 Jul 2017 12:11:39 -0400 Received: from lb1.openmailbox.org ([5.79.108.160]:58672 helo=mail.openmailbox.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1da2Ql-0001t1-Gz for 27461@debbugs.gnu.org; Tue, 25 Jul 2017 12:11:35 -0400 Received: by mail.openmailbox.org (Postfix, from userid 20002) id D79224E3E3D; Tue, 25 Jul 2017 18:11:29 +0200 (CEST) DKIM-Signature: v=1; a=rsa-sha256; c=simple/simple; d=openmailbox.org; s=openmailbox; t=1500999090; bh=SgQ4HC7VeQsJMMKy7kUwRGb/6xIXQ7NaED2H86eQV88=; h=From:To:Cc:Subject:Date:In-Reply-To:References:From; b=wnPt0/1tVxObB+7wQkw6YU0SG1TRwUNSQbNGtJIfcZsS04YQtFMavKOxQVChFIB39 QPPZFln3woQoqX1deykQy0lDHRVR19vsmB/r4ABA2m29MzyKwl0o++1463oiq/YPFr AV3nYYNqcsv21JnMxM+B8t1eDqJ5Sx78y6nH0gQk= X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on ZDZR003 X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=NO_RECEIVED,NO_RELAYS, T_DKIM_INVALID autolearn=disabled version=3.4.0 From: Theodoros Foradis DKIM-Signature: v=1; a=rsa-sha256; c=simple/simple; d=openmailbox.org; s=openmailbox; t=1500999088; bh=SgQ4HC7VeQsJMMKy7kUwRGb/6xIXQ7NaED2H86eQV88=; h=From:To:Cc:Subject:Date:In-Reply-To:References:From; b=r91rpyKY8Yv7E4gbz07gFQvQM7wTkJ7lxAi50OdbA9FRbATEev7nEXAp0oUfqRdF5 DGldQgtZYQUUC4JSZ4CFrR6gh02sX6MN4TlF5Fh4Fqay2PdHtOLAX/Nb7R/uE3luCz flL2LpUrlsPwWNOPNYLJvq5tJ78UCj3VukGwtnsY= To: 27461@debbugs.gnu.org Subject: [PATCH v2 2/2] gnu: Add python2-z3. Date: Tue, 25 Jul 2017 19:11:13 +0300 Message-Id: <20170725161113.26165-2-theodoros.for@openmailbox.org> X-Mailer: git-send-email 2.13.2 In-Reply-To: <20170725161113.26165-1-theodoros.for@openmailbox.org> References: <8760enxy1o.fsf@gnu.org> <20170725161113.26165-1-theodoros.for@openmailbox.org> X-Spam-Score: 0.5 (/) X-Debbugs-Envelope-To: 27461 Cc: ludo@gnu.org, julien@lepiller.eu X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: 0.5 (/) From: Julien Lepiller * gnu/packages/python.scm (python2-z3): New variable. --- gnu/packages/python.scm | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) diff --git a/gnu/packages/python.scm b/gnu/packages/python.scm index 6e1e289e9..b06cbd218 100644 --- a/gnu/packages/python.scm +++ b/gnu/packages/python.scm @@ -15512,3 +15512,33 @@ pure Python module.") (define-public python2-rencode (package-with-python2 python-rencode)) + +(define-public python2-z3 + (package + (inherit z3) + (name "python2-z3") + (build-system python-build-system) + (propagated-inputs + `(("z3" ,z3))) + (arguments + `(#:python ,python-2 + #:phases + (modify-phases %standard-phases + (add-before 'build 'prepare + (lambda* (#:key inputs #:allow-other-keys) + (system* "python" "scripts/mk_make.py") + (copy-file "build/python/z3/z3core.py" + "src/api/python/z3/z3core.py") + (copy-file "build/python/z3/z3consts.py" + "src/api/python/z3/z3consts.py") + (chdir "src/api/python") + (substitute* "z3/z3core.py" + (("_dirs = \\[") + (string-append "_dirs = ['" (assoc-ref inputs "z3") + "/lib', "))) + (substitute* "MANIFEST.in" + ((".*") "")) + (substitute* "setup.py" + (("self.execute\\(.*") "\n") + (("scripts=.*") "\n")) + #t))))))) -- 2.13.2 From debbugs-submit-bounces@debbugs.gnu.org Sat Jul 29 17:00:18 2017 Received: (at 27461) by debbugs.gnu.org; 29 Jul 2017 21:00:18 +0000 Received: from localhost ([127.0.0.1]:33418 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dbYqQ-0002z0-JT for submit@debbugs.gnu.org; Sat, 29 Jul 2017 17:00:18 -0400 Received: from eggs.gnu.org ([208.118.235.92]:38488) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dbYqO-0002ym-IV for 27461@debbugs.gnu.org; Sat, 29 Jul 2017 17:00:17 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1dbYqI-0001B2-GQ for 27461@debbugs.gnu.org; Sat, 29 Jul 2017 17:00:11 -0400 X-Spam-Checker-Version: SpamAssassin 3.3.2 (2011-06-06) on eggs.gnu.org X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,RP_MATCHES_RCVD autolearn=disabled version=3.3.2 Received: from fencepost.gnu.org ([2001:4830:134:3::e]:41772) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1dbYqA-0000xt-3E; Sat, 29 Jul 2017 17:00:02 -0400 Received: from reverse-83.fdn.fr ([80.67.176.83]:56960 helo=ribbon) by fencepost.gnu.org with esmtpsa (TLS1.2:RSA_AES_256_CBC_SHA1:256) (Exim 4.82) (envelope-from ) id 1dbYq9-000642-Hr; Sat, 29 Jul 2017 17:00:01 -0400 From: ludo@gnu.org (Ludovic =?utf-8?Q?Court=C3=A8s?=) To: Theodoros Foradis Subject: Re: [bug#27461] [PATCH v2 1/2] gnu: Add z3. References: <8760enxy1o.fsf@gnu.org> <20170725161113.26165-1-theodoros.for@openmailbox.org> Date: Sat, 29 Jul 2017 22:59:56 +0200 In-Reply-To: <20170725161113.26165-1-theodoros.for@openmailbox.org> (Theodoros Foradis's message of "Tue, 25 Jul 2017 19:11:12 +0300") Message-ID: <87inibgdrn.fsf@gnu.org> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/25.2 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Received-From: 2001:4830:134:3::e X-Spam-Score: -5.0 (-----) X-Debbugs-Envelope-To: 27461 Cc: julien@lepiller.eu, 27461@debbugs.gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -5.0 (-----) Hi Theodoros, Theodoros Foradis skribis: > * gnu/packages/maths.scm (z3): New variable. > * gnu/packages/fpga.scm (yosys): Add z3 to propagated-inputs. I splitted it into two patches (because these two things are unrelated), slightly expounded the z3 description, and committed. Thanks, Ludo=E2=80=99. From debbugs-submit-bounces@debbugs.gnu.org Sat Jul 29 17:03:39 2017 Received: (at 27461) by debbugs.gnu.org; 29 Jul 2017 21:03:39 +0000 Received: from localhost ([127.0.0.1]:33422 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dbYtY-00033t-1h for submit@debbugs.gnu.org; Sat, 29 Jul 2017 17:03:39 -0400 Received: from eggs.gnu.org ([208.118.235.92]:39032) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dbYtW-00033g-DY for 27461@debbugs.gnu.org; Sat, 29 Jul 2017 17:03:30 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1dbYtQ-0003QB-FL for 27461@debbugs.gnu.org; Sat, 29 Jul 2017 17:03:25 -0400 X-Spam-Checker-Version: SpamAssassin 3.3.2 (2011-06-06) on eggs.gnu.org X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,RP_MATCHES_RCVD autolearn=disabled version=3.3.2 Received: from fencepost.gnu.org ([2001:4830:134:3::e]:41823) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1dbYtJ-0003Kv-Jx; Sat, 29 Jul 2017 17:03:17 -0400 Received: from reverse-83.fdn.fr ([80.67.176.83]:56962 helo=ribbon) by fencepost.gnu.org with esmtpsa (TLS1.2:RSA_AES_256_CBC_SHA1:256) (Exim 4.82) (envelope-from ) id 1dbYtJ-0006aH-5L; Sat, 29 Jul 2017 17:03:17 -0400 From: ludo@gnu.org (Ludovic =?utf-8?Q?Court=C3=A8s?=) To: Theodoros Foradis Subject: Re: [bug#27461] [PATCH v2 2/2] gnu: Add python2-z3. References: <8760enxy1o.fsf@gnu.org> <20170725161113.26165-1-theodoros.for@openmailbox.org> <20170725161113.26165-2-theodoros.for@openmailbox.org> Date: Sat, 29 Jul 2017 23:03:14 +0200 In-Reply-To: <20170725161113.26165-2-theodoros.for@openmailbox.org> (Theodoros Foradis's message of "Tue, 25 Jul 2017 19:11:13 +0300") Message-ID: <87d18jgdm5.fsf@gnu.org> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/25.2 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Received-From: 2001:4830:134:3::e X-Spam-Score: -5.0 (-----) X-Debbugs-Envelope-To: 27461 Cc: julien@lepiller.eu, 27461@debbugs.gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -0.0 (/) Hi, Theodoros Foradis skribis: > From: Julien Lepiller > > * gnu/packages/python.scm (python2-z3): New variable. [...] > +(define-public python2-z3 > + (package > + (inherit z3) > + (name "python2-z3") Please add (synopsis "Python bindings to the Z3 theorem prover"). > + (build-system python-build-system) > + (propagated-inputs > + `(("z3" ,z3))) Can we avoid propagating it? > + (arguments > + `(#:python ,python-2 > + #:phases > + (modify-phases %standard-phases > + (add-before 'build 'prepare > + (lambda* (#:key inputs #:allow-other-keys) It would be nice to have comments in this procedure to help understand what=E2=80=99s going on. > + (system* "python" "scripts/mk_make.py") > + (copy-file "build/python/z3/z3core.py" > + "src/api/python/z3/z3core.py") > + (copy-file "build/python/z3/z3consts.py" > + "src/api/python/z3/z3consts.py") You can use (install-file "build/python/z3/z3consts.py" "src/api/python/z3"= ). > + (chdir "src/api/python") > + (substitute* "z3/z3core.py" > + (("_dirs =3D \\[") > + (string-append "_dirs =3D ['" (assoc-ref inputs "z3") > + "/lib', "))) > + (substitute* "MANIFEST.in" > + ((".*") "")) > + (substitute* "setup.py" > + (("self.execute\\(.*") "\n") > + (("scripts=3D.*") "\n")) > + #t))))))) Also, since Z3 already depends on Python, would it make sense to have a single package? Thanks, Ludo=E2=80=99. From debbugs-submit-bounces@debbugs.gnu.org Tue Aug 01 08:14:36 2017 Received: (at 27461) by debbugs.gnu.org; 1 Aug 2017 12:14:36 +0000 Received: from localhost ([127.0.0.1]:36208 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dcW4K-0003md-4X for submit@debbugs.gnu.org; Tue, 01 Aug 2017 08:14:36 -0400 Received: from dd1012.kasserver.com ([85.13.128.8]:60336) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dcW4I-0003mV-C6 for 27461@debbugs.gnu.org; Tue, 01 Aug 2017 08:14:34 -0400 Received: from localhost (77.118.188.11.wireless.dyn.drei.com [77.118.188.11]) by dd1012.kasserver.com (Postfix) with ESMTPSA id 2C8D61CA0360; Tue, 1 Aug 2017 14:14:31 +0200 (CEST) Date: Tue, 1 Aug 2017 14:14:25 +0200 From: Danny Milosavljevic To: ludo@gnu.org (Ludovic =?ISO-8859-1?Q?Court=E8s?=) Subject: Re: [bug#27461] [PATCH v2 1/2] gnu: Add z3. Message-ID: <20170801141425.53914980@scratchpost.org> In-Reply-To: <87inibgdrn.fsf@gnu.org> References: <8760enxy1o.fsf@gnu.org> <20170725161113.26165-1-theodoros.for@openmailbox.org> <87inibgdrn.fsf@gnu.org> X-Mailer: Claws Mail 3.15.0-dirty (GTK+ 2.24.31; x86_64-unknown-linux-gnu) MIME-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit X-Spam-Score: -0.7 (/) X-Debbugs-Envelope-To: 27461 Cc: 27461@debbugs.gnu.org, Theodoros Foradis X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -0.7 (/) z3 fails to build on ARMHF, see . >ld: api/dll/mem_initializer.o: relocation R_ARM_THM_MOVW_ABS_NC against `a local symbol' can not be used when making a shared object; recompile with -fPIC. There's https://github.com/Z3Prover/z3/issues/585 which says essentially that one should use "cmake", then the problem doesn't appear. From debbugs-submit-bounces@debbugs.gnu.org Tue Aug 01 08:30:33 2017 Received: (at 27461) by debbugs.gnu.org; 1 Aug 2017 12:30:33 +0000 Received: from localhost ([127.0.0.1]:36226 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dcWJl-0004B3-0u for submit@debbugs.gnu.org; Tue, 01 Aug 2017 08:30:33 -0400 Received: from eggs.gnu.org ([208.118.235.92]:43052) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dcWJj-0004Ap-9m for 27461@debbugs.gnu.org; Tue, 01 Aug 2017 08:30:31 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1dcWJa-0000Rn-0u for 27461@debbugs.gnu.org; Tue, 01 Aug 2017 08:30:26 -0400 X-Spam-Checker-Version: SpamAssassin 3.3.2 (2011-06-06) on eggs.gnu.org X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,RP_MATCHES_RCVD autolearn=disabled version=3.3.2 Received: from fencepost.gnu.org ([2001:4830:134:3::e]:53559) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1dcWJZ-0000Ri-TS; Tue, 01 Aug 2017 08:30:21 -0400 Received: from [193.50.110.251] (port=38348 helo=ribbon) by fencepost.gnu.org with esmtpsa (TLS1.2:RSA_AES_256_CBC_SHA1:256) (Exim 4.82) (envelope-from ) id 1dcWJZ-0006Mm-9t; Tue, 01 Aug 2017 08:30:21 -0400 From: ludo@gnu.org (Ludovic =?utf-8?Q?Court=C3=A8s?=) To: Danny Milosavljevic Subject: Re: [bug#27461] [PATCH v2 1/2] gnu: Add z3. References: <8760enxy1o.fsf@gnu.org> <20170725161113.26165-1-theodoros.for@openmailbox.org> <87inibgdrn.fsf@gnu.org> <20170801141425.53914980@scratchpost.org> X-URL: http://www.fdn.fr/~lcourtes/ X-Revolutionary-Date: 14 Thermidor an 225 de la =?utf-8?Q?R=C3=A9volution?= X-PGP-Key-ID: 0x090B11993D9AEBB5 X-PGP-Key: http://www.fdn.fr/~lcourtes/ludovic.asc X-PGP-Fingerprint: 3CE4 6455 8A84 FDC6 9DB4 0CFB 090B 1199 3D9A EBB5 X-OS: x86_64-unknown-linux-gnu Date: Tue, 01 Aug 2017 14:30:18 +0200 In-Reply-To: <20170801141425.53914980@scratchpost.org> (Danny Milosavljevic's message of "Tue, 1 Aug 2017 14:14:25 +0200") Message-ID: <8760e7pj1h.fsf@gnu.org> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/25.2 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Received-From: 2001:4830:134:3::e X-Spam-Score: -5.0 (-----) X-Debbugs-Envelope-To: 27461 Cc: 27461@debbugs.gnu.org, Theodoros Foradis X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -5.0 (-----) Hello, Danny Milosavljevic skribis: > z3 fails to build on ARMHF, see . > >>ld: api/dll/mem_initializer.o: relocation R_ARM_THM_MOVW_ABS_NC against `= a local symbol' can not be used when making a shared object; recompile with= -fPIC. > > There's https://github.com/Z3Prover/z3/issues/585 which says essentially = that one should use "cmake", then the problem doesn't appear. Oh, thanks for the heads-up. Theodoros, would you consider writing a patch switching from =E2=80=98gnu-build-system=E2=80=99 to =E2=80=98cmake-build-system=E2=80=99? Thanks, Ludo=E2=80=99. From debbugs-submit-bounces@debbugs.gnu.org Wed Aug 02 06:04:35 2017 Received: (at 27461) by debbugs.gnu.org; 2 Aug 2017 10:04:35 +0000 Received: from localhost ([127.0.0.1]:37730 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dcqW3-0005eU-Ct for submit@debbugs.gnu.org; Wed, 02 Aug 2017 06:04:35 -0400 Received: from lb1.openmailbox.org ([5.79.108.160]:40483 helo=mail.openmailbox.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dcqW0-0005eK-4z for 27461@debbugs.gnu.org; Wed, 02 Aug 2017 06:04:32 -0400 Received: by mail.openmailbox.org (Postfix, from userid 20002) id DE8BC4E52D6; Wed, 2 Aug 2017 12:04:29 +0200 (CEST) DKIM-Signature: v=1; a=rsa-sha256; c=simple/simple; d=openmailbox.org; s=openmailbox; t=1501668270; bh=C+FmCE+SS8fDiOJKjlIAGVXna/YqfPLAZ2aW0+FmMfo=; h=References:From:To:Subject:In-reply-to:Date:From; b=NCiDLaw5FyGOQgN6sjbRMML/THvQcWD54hgS/+faPFsIwBnOh918Qa5pmj0eOU38G bLS24aPdJW94bFuIurP7zu0M8oL3o/J8Th5x3Y9SWFcMdsVwxjduFGwk23zGrNEc2o Vz7LwR0nP5LV9pf+uK1ovazO4QdBRdK4mnNA5oR4= X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on ZDZR002 X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=NO_RECEIVED,NO_RELAYS, T_DKIM_INVALID autolearn=disabled version=3.4.0 References: <8760enxy1o.fsf@gnu.org> <20170725161113.26165-1-theodoros.for@openmailbox.org> <87inibgdrn.fsf@gnu.org> <20170801141425.53914980@scratchpost.org> <8760e7pj1h.fsf@gnu.org> DKIM-Signature: v=1; a=rsa-sha256; c=simple/simple; d=openmailbox.org; s=openmailbox; t=1501668269; bh=C+FmCE+SS8fDiOJKjlIAGVXna/YqfPLAZ2aW0+FmMfo=; h=References:From:To:Subject:In-reply-to:Date:From; b=z6cQnsNMy5QGF8PTa+f0Aj5AX8MNw3+Q/b3EXRzXzOkJKNRzOviHUqxb7lWb+zNwn eu4iYCUVcotoJEwZFDX5SrWw443a9NHFAq1X9XVbGxmMc6HbLBIGlx7xn8j2YMw9BG eoYs53kTtTJZ5krefozgYd4UaYulwaKAd5GouIsQ= User-agent: mu4e 0.9.18; emacs 25.2.1 From: Theodoros Foradis To: 27461@debbugs.gnu.org Subject: Re: [bug#27461] [PATCH v2 1/2] gnu: Add z3. Message-ID: <87tw1q2sp7.fsf@openmailbox.org> In-reply-to: <8760e7pj1h.fsf@gnu.org> Date: Wed, 02 Aug 2017 13:04:14 +0300 MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 8bit X-Spam-Score: 0.0 (/) X-Debbugs-Envelope-To: 27461 X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: 0.0 (/) Hello, > Theodoros, would you consider writing a patch switching from > ‘gnu-build-system’ to ‘cmake-build-system’? I am replying with a patch, changing the build system to cmake, and adding the python bindings in the same package. The package does not propagate python. I need someone to test the python bindings, because I am not a python user myself. Regards, -- Theodoros Foradis From debbugs-submit-bounces@debbugs.gnu.org Wed Aug 02 06:10:40 2017 Received: (at 27461) by debbugs.gnu.org; 2 Aug 2017 10:10:40 +0000 Received: from localhost ([127.0.0.1]:37745 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dcqbw-0005nF-I1 for submit@debbugs.gnu.org; Wed, 02 Aug 2017 06:10:40 -0400 Received: from lb1.openmailbox.org ([5.79.108.160]:56714 helo=mail.openmailbox.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dcqbu-0005n7-Um for 27461@debbugs.gnu.org; Wed, 02 Aug 2017 06:10:39 -0400 Received: by mail.openmailbox.org (Postfix, from userid 20002) id 4FF584E9B45; Wed, 2 Aug 2017 12:10:37 +0200 (CEST) DKIM-Signature: v=1; a=rsa-sha256; c=simple/simple; d=openmailbox.org; s=openmailbox; t=1501668638; bh=0m5wIQ1Yp+7D7WpC+0m0SxuOu5dwi7afgO8rMFr1O2U=; h=From:To:Cc:Subject:Date:In-Reply-To:References:From; b=gdslnqfytahRvZ79RFNJjPNrZ71KPKgw7AikZLsiYvzfr1TcTVPpwWsBZc3hRP4pU 2SYFjuLnoQydIeEffTb6sKG612JOKNOL+8UVJIY2/komXH93nbuFcBGUFFSporetgG 6gk1fMTbeHyRizLkDpyQ8/rZFJDyiid+2GosbJt8= X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on ZDZR003 X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=NO_RECEIVED,NO_RELAYS, T_DKIM_INVALID,URIBL_BLOCKED autolearn=disabled version=3.4.0 From: Theodoros Foradis DKIM-Signature: v=1; a=rsa-sha256; c=simple/simple; d=openmailbox.org; s=openmailbox; t=1501668636; bh=0m5wIQ1Yp+7D7WpC+0m0SxuOu5dwi7afgO8rMFr1O2U=; h=From:To:Cc:Subject:Date:In-Reply-To:References:From; b=huMt/HsF6ZGsmmjREFDRaCNYL0BOczUgPLN2shPyWVQpRMu6vf9qyIrGJCWsnuMt6 4y9/u19YVTOVkPe//m0oQ2gO5YeAzHEr4EGhU1VOZe3L7CwTJ4RcHY4FFKtZd0QhCg o3YPac2J+GJOY/BS9j3ksgrXcpzSpqyrfrXzB+m8= To: 27461@debbugs.gnu.org Subject: [PATCH] gnu: Add python bindings to z3. Date: Wed, 2 Aug 2017 13:10:12 +0300 Message-Id: <20170802101012.29210-1-theodoros.for@openmailbox.org> X-Mailer: git-send-email 2.13.2 In-Reply-To: <87tw1q2sp7.fsf@openmailbox.org> References: <87tw1q2sp7.fsf@openmailbox.org> X-Spam-Score: 0.0 (/) X-Debbugs-Envelope-To: 27461 Cc: dannym@scratchpost.org, ludo@gnu.org, Theodoros Foradis X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: 0.0 (/) * 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 From debbugs-submit-bounces@debbugs.gnu.org Mon Aug 21 11:14:16 2017 Received: (at 27461-done) by debbugs.gnu.org; 21 Aug 2017 15:14:16 +0000 Received: from localhost ([127.0.0.1]:47974 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1djoPA-0000rB-LM for submit@debbugs.gnu.org; Mon, 21 Aug 2017 11:14:16 -0400 Received: from eggs.gnu.org ([208.118.235.92]:57014) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1djoP9-0000qy-HV for 27461-done@debbugs.gnu.org; Mon, 21 Aug 2017 11:14:15 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1djoP3-0007V0-Ao for 27461-done@debbugs.gnu.org; Mon, 21 Aug 2017 11:14:10 -0400 X-Spam-Checker-Version: SpamAssassin 3.3.2 (2011-06-06) on eggs.gnu.org X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,RP_MATCHES_RCVD autolearn=disabled version=3.3.2 Received: from fencepost.gnu.org ([2001:4830:134:3::e]:58217) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1djoOx-0007Sr-48; Mon, 21 Aug 2017 11:14:03 -0400 Received: from [193.50.110.251] (port=40282 helo=ribbon) by fencepost.gnu.org with esmtpsa (TLS1.2:RSA_AES_256_CBC_SHA1:256) (Exim 4.82) (envelope-from ) id 1djoOw-0008Bb-Oj; Mon, 21 Aug 2017 11:14:02 -0400 From: ludo@gnu.org (Ludovic =?utf-8?Q?Court=C3=A8s?=) To: Theodoros Foradis Subject: Re: [PATCH] gnu: Add python bindings to z3. References: <87tw1q2sp7.fsf@openmailbox.org> <20170802101012.29210-1-theodoros.for@openmailbox.org> X-URL: http://www.fdn.fr/~lcourtes/ X-Revolutionary-Date: 4 Fructidor an 225 de la =?utf-8?Q?R=C3=A9volution?= X-PGP-Key-ID: 0x090B11993D9AEBB5 X-PGP-Key: http://www.fdn.fr/~lcourtes/ludovic.asc X-PGP-Fingerprint: 3CE4 6455 8A84 FDC6 9DB4 0CFB 090B 1199 3D9A EBB5 X-OS: x86_64-unknown-linux-gnu Date: Mon, 21 Aug 2017 17:14:00 +0200 In-Reply-To: <20170802101012.29210-1-theodoros.for@openmailbox.org> (Theodoros Foradis's message of "Wed, 2 Aug 2017 13:10:12 +0300") Message-ID: <87d17pt0lj.fsf@gnu.org> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/25.2 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Received-From: 2001:4830:134:3::e X-Spam-Score: -5.0 (-----) X-Debbugs-Envelope-To: 27461-done Cc: 27461-done@debbugs.gnu.org, dannym@scratchpost.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -5.0 (-----) Hi Theodoros, And sorry for the long delay! Theodoros Foradis skribis: > * 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. I=E2=80=99ve applied this patch with a few modifications, in particular arranging to run the tests (disabling them altogether was not OK since we knew there is a test suite): https://git.savannah.gnu.org/cgit/guix.git/commit/?id=3Dcf684d87d7446ffe3= 3ca4c73bf51dc24fa5a7129 Thanks, Ludo=E2=80=99. From unknown Mon Jun 23 16:45:08 2025 Received: (at fakecontrol) by fakecontrolmessage; To: internal_control@debbugs.gnu.org From: Debbugs Internal Request Subject: Internal Control Message-Id: bug archived. Date: Tue, 19 Sep 2017 11:24:05 +0000 User-Agent: Fakemail v42.6.9 # This is a fake control message. # # The action: # bug archived. thanks # This fakemail brought to you by your local debbugs # administrator