[bug#27461] [PATCH] gnu: Add z3.

[julien lepiller <julien@lepiller.eu>]

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 <dannym@scratchpost.org>
> -;;; Copyright © 2016 Theodoros Foradis <theodoros.for@openmailbox.org>
> +;;; Copyright © 2016, 2017 Theodoros Foradis 
> <theodoros.for@openmailbox.org>
>  ;;;
>  ;;; 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 
> <pgarlick@tourbillion-technology.com>
>  ;;; Copyright © 2017 ng0 <contact.ng0@cryptolab.net>
>  ;;; Copyright © 2017 Ben Woodcroft <donttrustben@gmail.com>
> +;;; Copyright © 2017 Theodoros Foradis <theodoros.for@openmailbox.org>
>  ;;;
>  ;;; 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) ))