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

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

[Theodoros Foradis]

* 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) ))
-- 
2.13.1

[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 <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) ))

[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

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

[Ludovic Courtès]

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’.

[bug#27461] [PATCH v2 1/2] gnu: Add z3.

[Theodoros Foradis]

* 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 5e4cd8586..536fb9bed 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.
 ;;;
@@ -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

[bug#27461] [PATCH v2 2/2] gnu: Add python2-z3.

[Theodoros Foradis]

From: Julien Lepiller <julien@lepiller.eu>

* 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

[bug#27461] [PATCH v2 2/2] gnu: Add python2-z3.

[Ludovic Courtès]

Hi,

Theodoros Foradis <theodoros.for@openmailbox.org> skribis:

> From: Julien Lepiller <julien@lepiller.eu>
>
> * 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’s 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 = \\[")
> +                 (string-append "_dirs = ['" (assoc-ref inputs "z3")
> +                                "/lib', ")))
> +              (substitute* "MANIFEST.in"
> +                ((".*") ""))
> +              (substitute* "setup.py"
> +                (("self.execute\\(.*") "\n")
> +                (("scripts=.*") "\n"))
> +              #t)))))))

Also, since Z3 already depends on Python, would it make sense to have a
single package?

Thanks,
Ludo’.

[bug#27461] [PATCH v2 1/2] gnu: Add z3.

[Ludovic Courtès]

Hi Theodoros,

Theodoros Foradis <theodoros.for@openmailbox.org> 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’.

[bug#27461] [PATCH v2 1/2] gnu: Add z3.

[Danny Milosavljevic]

z3 fails to build on ARMHF, see <http://hydra.gnu.org/build/2204789/nixlog/1>.

>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.

[bug#27461] [PATCH v2 1/2] gnu: Add z3.

[Ludovic Courtès]

Hello,

Danny Milosavljevic <dannym@scratchpost.org> skribis:

> z3 fails to build on ARMHF, see <http://hydra.gnu.org/build/2204789/nixlog/1>.
>
>>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
‘gnu-build-system’ to ‘cmake-build-system’?

Thanks,
Ludo’.

[bug#27461] [PATCH v2 1/2] gnu: Add z3.

[Theodoros Foradis]

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

[bug#27461] [PATCH] gnu: Add python bindings to z3.

[Theodoros Foradis]

* gnu/packages/maths.scm (z3): Add python bindings.
[build-system]: Change to cmake-build-system.
[arguments]<phases>: Remove "changedir" phase.
                     Add "bootstrap" phase.
[arguments]<configure-flags>: Add them.
[arguments]<tests>: 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

bug#27461: [PATCH] gnu: Add python bindings to z3.

[Ludovic Courtès]

Hi Theodoros,

And sorry for the long delay!

Theodoros Foradis <theodoros.for@openmailbox.org> skribis:

> * gnu/packages/maths.scm (z3): Add python bindings.
> [build-system]: Change to cmake-build-system.
> [arguments]<phases>: Remove "changedir" phase.
>                      Add "bootstrap" phase.
> [arguments]<configure-flags>: Add them.
> [arguments]<tests>: Disable tests.

I’ve 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=cf684d87d7446ffe33ca4c73bf51dc24fa5a7129

Thanks,
Ludo’.