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

[julien lepiller]

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 <address@hidden>
> -;;; Copyright © 2016 Theodoros Foradis <address@hidden>
> +;;; Copyright © 2016, 2017 Theodoros Foradis 
> <address@hidden>
>  ;;;
>  ;;; 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 
> <address@hidden>
>  ;;; Copyright © 2017 ng0 <address@hidden>
>  ;;; Copyright © 2017 Ben Woodcroft <address@hidden>
> +;;; Copyright © 2017 Theodoros Foradis <address@hidden>
>  ;;;
>  ;;; 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) ))