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

[Theodoros Foradis]

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