From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from eggs.gnu.org ([2001:4830:134:3::10]:52850) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1dP2n4-0002x5-1G for guix-patches@gnu.org; Sun, 25 Jun 2017 04:21:07 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1dP2n0-0003X8-FU for guix-patches@gnu.org; Sun, 25 Jun 2017 04:21:06 -0400 Received: from debbugs.gnu.org ([208.118.235.43]:33598) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1dP2n0-0003Wv-B6 for guix-patches@gnu.org; Sun, 25 Jun 2017 04:21:02 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1dP2n0-00053D-5H for guix-patches@gnu.org; Sun, 25 Jun 2017 04:21:02 -0400 Subject: [bug#27461] [PATCH] gnu: Add z3. Resent-Message-ID: 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 In-Reply-To: <20170623155022.16252-1-theodoros.for@openmailbox.org> References: <20170623155022.16252-1-theodoros.for@openmailbox.org> Message-ID: <85aa5980dfa7244056fdd3726cc60ad1@lepiller.eu> 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 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) ))