[bug#33764] [PATCH] gnu: z3: Update to 4.8.3 and add python{, 2}-z3 bindings.

[bug#33764] [PATCH] gnu: z3: Update to 4.8.3 and add python{, 2}-z3 bindings.

[Amin Bandali]

* gnu/packages/maths.scm (z3): Update to 4.8.3.
[build-system]: Switch from cmake to make, and use the current
scripts/mk_make.py build script instead of the now-deprecated
contrib/cmake/bootstrap.py.

* gnu/packages/python.scm (python-z3, python2-z3): New public
variables.
---
 gnu/packages/maths.scm  | 31 +++++++++++++++++++------------
 gnu/packages/python.scm | 10 ++++++++++
 2 files changed, 29 insertions(+), 12 deletions(-)

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index ad6aacf9c..7996c3211 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -29,6 +29,7 @@
 ;;; Copyright © 2018 Marius Bakke <mbakke@fastmail.com>
 ;;; Copyright © 2018 Eric Brown <brown@fastmail.com>
 ;;; Copyright © 2018 Julien Lepiller <julien@lepiller.eu>
+;;; Copyright © 2018 Amin Bandali <bandali@gnu.org>
 ;;;
 ;;; This file is part of GNU Guix.
 ;;;
@@ -3965,7 +3966,7 @@ as equations, scalars, vectors, and matrices.")
 (define-public z3
   (package
     (name "z3")
-    (version "4.8.1")
+    (version "4.8.3")
     (home-page "https://github.com/Z3Prover/z3")
     (source (origin
               (method git-fetch)
@@ -3973,21 +3974,26 @@ as equations, scalars, vectors, and matrices.")
                                   (commit (string-append "z3-" version))))
               (sha256
                (base32
-                "1vr57bwx40sd5riijyrhy70i2wnv9xrdihf6y5zdz56yq88rl48f"))))
-    (build-system cmake-build-system)
+                "0p5gdmhd32x6zwmx7j5cgwh4jyfxa9yapym95nlmyfaqzak92qar"))))
+    (build-system gnu-build-system)
     (arguments
-     `(#:configure-flags
-       (list "-DBUILD_PYTHON_BINDINGS=true"
-             "-DINSTALL_PYTHON_BINDINGS=true"
-             (string-append "-DCMAKE_INSTALL_PYTHON_PKG_DIR="
-                            %output
-                            "/lib/python2.7/site-packages"))
-       #:phases
+     `(#:phases
        (modify-phases %standard-phases
          (add-before 'configure 'bootstrap
            (lambda _
              (zero?
-              (system* "python" "contrib/cmake/bootstrap.py" "create"))))
+              (system* "python" "scripts/mk_make.py"))))
+         ;; work around gnu-build-system's setting --enable-fast-install
+         ;; (z3's `configure' is a wrapper around the above python file,
+         ;; which fails when passed --enable-fast-install)
+         (replace 'configure
+           (lambda* (#:key inputs outputs #:allow-other-keys)
+             (invoke "./configure"
+                     (string-append "--prefix=" (assoc-ref outputs "out")))))
+         (add-after 'configure 'change-directory
+           (lambda _
+             (chdir "build")
+             #t))
          (add-before 'check 'make-test-z3
            (lambda _
              ;; Build the test suite executable.
@@ -3998,7 +4004,8 @@ as equations, scalars, vectors, and matrices.")
              ;; Run all the tests that don't require arguments.
              (zero? (system* "./test-z3" "/a")))))))
     (native-inputs
-     `(("python" ,python-2)))
+     `(("which" ,(@ (gnu packages base) which))
+       ("python" ,python-wrapper)))
     (synopsis "Theorem prover")
     (description "Z3 is a theorem prover and @dfn{satisfiability modulo
 theories} (SMT) solver.  It provides a C/C++ API, as well as Python bindings.")
diff --git a/gnu/packages/python.scm b/gnu/packages/python.scm
index fd13339cc..5db3c438e 100644
--- a/gnu/packages/python.scm
+++ b/gnu/packages/python.scm
@@ -56,6 +56,7 @@
 ;;; Copyright © 2018 Clément Lassieur <clement@lassieur.org>
 ;;; Copyright © 2018 Maxim Cournoyer <maxim.cournoyer@gmail.com>
 ;;; Copyright © 2018 Luther Thompson <lutheroto@gmail.com>
+;;; Copyright © 2018 Amin Bandali <bandali@gnu.org>
 ;;;
 ;;; This file is part of GNU Guix.
 ;;;
@@ -14989,3 +14990,12 @@ RFC 8265 and RFC 8266.")
     (description "Simple decorator to set attributes of target function or
 class in a @acronym{DRY, Don't Repeat Yourself} way.")
     (license license:expat)))
+
+(define-public python-z3 z3)
+
+(define-public python2-z3
+  (package (inherit python-z3)
+    (name "python2-z3")
+    (native-inputs
+     `(("which" ,which)
+       ("python" ,python-2)))))
-- 
2.20.0

[bug#33764] [PATCH] gnu: z3: Update to 4.8.3 and add python{, 2}-z3 bindings.

[Ludovic Courtès]

Hello Amin,

Amin Bandali <bandali@gnu.org> skribis:

> * gnu/packages/maths.scm (z3): Update to 4.8.3.
> [build-system]: Switch from cmake to make, and use the current
> scripts/mk_make.py build script instead of the now-deprecated
> contrib/cmake/bootstrap.py.
>
> * gnu/packages/python.scm (python-z3, python2-z3): New public
> variables.

Overall LGTM.  Some comments:

>      (native-inputs
> -     `(("python" ,python-2)))
> +     `(("which" ,(@ (gnu packages base) which))
> +       ("python" ,python-wrapper)))

Please add #:use-module (gnu packages which) so you don’t have to resort
to the @ notation.

> --- a/gnu/packages/python.scm
> +++ b/gnu/packages/python.scm
> @@ -56,6 +56,7 @@
>  ;;; Copyright © 2018 Clément Lassieur <clement@lassieur.org>
>  ;;; Copyright © 2018 Maxim Cournoyer <maxim.cournoyer@gmail.com>
>  ;;; Copyright © 2018 Luther Thompson <lutheroto@gmail.com>
> +;;; Copyright © 2018 Amin Bandali <bandali@gnu.org>
>  ;;;
>  ;;; This file is part of GNU Guix.
>  ;;;
> @@ -14989,3 +14990,12 @@ RFC 8265 and RFC 8266.")
>      (description "Simple decorator to set attributes of target function or
>  class in a @acronym{DRY, Don't Repeat Yourself} way.")
>      (license license:expat)))
> +
> +(define-public python-z3 z3)

Is this variable necessary?  Note that this does not create a
“python-z3” package.

> +(define-public python2-z3
> +  (package (inherit python-z3)

This definition cannot be in python.scm; it must be in the same file as
‘z3’ or we can get “unbound variable” errors while loading either of
these two modules.

Also, as we’re approaching end-of-life upstream for Python 2.x, we now
avoid creating “python2-” packages, unless we cannot avoid it for some
reason.  Do you think we could do without this “python2-z3” package?

Could you send an updated patch?  If you think we really need
“python2-z3”, please make it a separate patch.

Thank you!

Ludo’.

[bug#33764] [PATCH] gnu: z3: Update to 4.8.3 and add python{, 2}-z3 bindings.

[Efraim Flashner]

[-- Attachment #1: Type: text/plain, Size: 2593 bytes --]

On Sun, Dec 16, 2018 at 04:18:16PM +0100, Ludovic Courtès wrote:
> Hello Amin,
> 
> Amin Bandali <bandali@gnu.org> skribis:
> 
> > * gnu/packages/maths.scm (z3): Update to 4.8.3.
> > [build-system]: Switch from cmake to make, and use the current
> > scripts/mk_make.py build script instead of the now-deprecated
> > contrib/cmake/bootstrap.py.
> >
> > * gnu/packages/python.scm (python-z3, python2-z3): New public
> > variables.
> 
> Overall LGTM.  Some comments:
> 
> >      (native-inputs
> > -     `(("python" ,python-2)))
> > +     `(("which" ,(@ (gnu packages base) which))
> > +       ("python" ,python-wrapper)))
> 
> Please add #:use-module (gnu packages which) so you don’t have to resort
> to the @ notation.
> 
> > --- a/gnu/packages/python.scm
> > +++ b/gnu/packages/python.scm
> > @@ -56,6 +56,7 @@
> >  ;;; Copyright © 2018 Clément Lassieur <clement@lassieur.org>
> >  ;;; Copyright © 2018 Maxim Cournoyer <maxim.cournoyer@gmail.com>
> >  ;;; Copyright © 2018 Luther Thompson <lutheroto@gmail.com>
> > +;;; Copyright © 2018 Amin Bandali <bandali@gnu.org>
> >  ;;;
> >  ;;; This file is part of GNU Guix.
> >  ;;;
> > @@ -14989,3 +14990,12 @@ RFC 8265 and RFC 8266.")
> >      (description "Simple decorator to set attributes of target function or
> >  class in a @acronym{DRY, Don't Repeat Yourself} way.")
> >      (license license:expat)))
> > +
> > +(define-public python-z3 z3)
> 
> Is this variable necessary?  Note that this does not create a
> “python-z3” package.
> 
> > +(define-public python2-z3
> > +  (package (inherit python-z3)
> 
> This definition cannot be in python.scm; it must be in the same file as
> ‘z3’ or we can get “unbound variable” errors while loading either of
> these two modules.
> 
> Also, as we’re approaching end-of-life upstream for Python 2.x, we now
> avoid creating “python2-” packages, unless we cannot avoid it for some
> reason.  Do you think we could do without this “python2-z3” package?
> 

Currently our z3 package builds python2 bindings

> Could you send an updated patch?  If you think we really need
> “python2-z3”, please make it a separate patch.
> 
> Thank you!
> 
> Ludo’.
> 

We should also check that the other packages that use z3 aren't
expecting the python2 bindings when built with the python3 bindings.

-- 
Efraim Flashner   <efraim@flashner.co.il>   אפרים פלשנר
GPG key = A28B F40C 3E55 1372 662D  14F7 41AA E7DC CA3D 8351
Confidentiality cannot be guaranteed on emails sent or received unencrypted

[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 833 bytes --]

[bug#33764] [PATCH] gnu: z3: Update to 4.8.3 and add python{, 2}-z3 bindings.

[Amin Bandali]

Hi Ludo’, Efraim,

Thank you both for the feedback.  I’ve responded below.

On 2018-12-17  9:29 AM, Efraim Flashner wrote:
> On Sun, Dec 16, 2018 at 04:18:16PM +0100, Ludovic Courtès wrote:
>> >      (native-inputs
>> > -     `(("python" ,python-2)))
>> > +     `(("which" ,(@ (gnu packages base) which))
>> > +       ("python" ,python-wrapper)))
>> 
>> Please add #:use-module (gnu packages which) so you don’t have to resort
>> to the @ notation.

Will do for the next version of the patch, thanks.

>> > +(define-public python-z3 z3)
>> 
>> Is this variable necessary?  Note that this does not create a
>> “python-z3” package.

I see!  I thought that it /would/ create a python-z3 package; but then
again I’m very much a Guix newb :) Since I added a python2-z3, I thought
I would also add a python-z3 for ‘symmetry’ in case someone expects it.

Should I then add a (define-public python-z3 (package inherit z3)) if we
decide to add the python2-z3 bindings?

>> > +(define-public python2-z3
>> > +  (package (inherit python-z3)
>> 
>> This definition cannot be in python.scm; it must be in the same file as
>> ‘z3’ or we can get “unbound variable” errors while loading either of
>> these two modules.

Oh I see.  If we choose to keep it (add it), I’ll move it to maths.scm.

>> Also, as we’re approaching end-of-life upstream for Python 2.x, we now
>> avoid creating “python2-” packages, unless we cannot avoid it for some
>> reason.  Do you think we could do without this “python2-z3” package?
>> 
>
> Currently our z3 package builds python2 bindings

What Efraim said.  Since the current z3 provides python2 bindings, I
thought I would preserve that option by adding a python2-z3 in case
anyone wants to continue to use the python2 bindings.

I’m Cc’ing Marius who’s one of the recent committers to the z3 package
definition.  Marius, any thoughts on whether we should keep the python2
bindings around or do away with them?

>> Could you send an updated patch?  If you think we really need
>> “python2-z3”, please make it a separate patch.

Sure.  I’ll send an update patch (or patches) once we figure out whether
we should keep the python2 bindings around.

>
> We should also check that the other packages that use z3 aren't
> expecting the python2 bindings when built with the python3 bindings.
>

Right.  grepping through the codebase, I see that only two other
packages depend on z3: cubicle (in maths.scm) and yosys (in fpga.scm).
cubicle is an ocaml package and doesn’t seem to use the python bindings
of z3, and yosys seems to only use z3 as an executable, not a library.

So, it appears to me that as of now, there are no packages that depend
on the python2 bindings of z3.  If so, do we drop python2-z3 (and also
python-z3) altogether and just switch z3 to python3?


Best,
amin

[bug#33764] [PATCH] gnu: z3: Update to 4.8.3 and add python{, 2}-z3 bindings.

[Ludovic Courtès]

Hello!

Amin Bandali <bandali@gnu.org> skribis:

> On 2018-12-17  9:29 AM, Efraim Flashner wrote:
>> On Sun, Dec 16, 2018 at 04:18:16PM +0100, Ludovic Courtès wrote:

[...]

>>> > +(define-public python2-z3
>>> > +  (package (inherit python-z3)
>>> 
>>> This definition cannot be in python.scm; it must be in the same file as
>>> ‘z3’ or we can get “unbound variable” errors while loading either of
>>> these two modules.
>
> Oh I see.  If we choose to keep it (add it), I’ll move it to maths.scm.
>
>>> Also, as we’re approaching end-of-life upstream for Python 2.x, we now
>>> avoid creating “python2-” packages, unless we cannot avoid it for some
>>> reason.  Do you think we could do without this “python2-z3” package?
>>> 
>>
>> Currently our z3 package builds python2 bindings
>
> What Efraim said.  Since the current z3 provides python2 bindings, I
> thought I would preserve that option by adding a python2-z3 in case
> anyone wants to continue to use the python2 bindings.
>
> I’m Cc’ing Marius who’s one of the recent committers to the z3 package
> definition.  Marius, any thoughts on whether we should keep the python2
> bindings around or do away with them?

Marius, WDYT?

Ludo’.

[bug#33764] [PATCH] gnu: z3: Update to 4.8.3 and add python{, 2}-z3 bindings.

[Marius Bakke]

[-- Attachment #1: Type: text/plain, Size: 1615 bytes --]

Ludovic Courtès <ludo@gnu.org> writes:

> Hello!
>
> Amin Bandali <bandali@gnu.org> skribis:
>
>> On 2018-12-17  9:29 AM, Efraim Flashner wrote:
>>> On Sun, Dec 16, 2018 at 04:18:16PM +0100, Ludovic Courtès wrote:
>
> [...]
>
>>>> > +(define-public python2-z3
>>>> > +  (package (inherit python-z3)
>>>> 
>>>> This definition cannot be in python.scm; it must be in the same file as
>>>> ‘z3’ or we can get “unbound variable” errors while loading either of
>>>> these two modules.
>>
>> Oh I see.  If we choose to keep it (add it), I’ll move it to maths.scm.
>>
>>>> Also, as we’re approaching end-of-life upstream for Python 2.x, we now
>>>> avoid creating “python2-” packages, unless we cannot avoid it for some
>>>> reason.  Do you think we could do without this “python2-z3” package?
>>>> 
>>>
>>> Currently our z3 package builds python2 bindings
>>
>> What Efraim said.  Since the current z3 provides python2 bindings, I
>> thought I would preserve that option by adding a python2-z3 in case
>> anyone wants to continue to use the python2 bindings.
>>
>> I’m Cc’ing Marius who’s one of the recent committers to the z3 package
>> definition.  Marius, any thoughts on whether we should keep the python2
>> bindings around or do away with them?
>
> Marius, WDYT?

Hello!

I don't actually know z3 at all, I just updated it to fix the build on
core-updates :-)

In any case dropping python2 bindings seems sensible, seeing as Python 2
is EOL in a year[1].  So please go ahead, thank you Amin!

[1]: https://www.python.org/dev/peps/pep-0373/

[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 487 bytes --]

[bug#33764] [PATCH] gnu: z3: Update to 4.8.3 and add python{, 2}-z3 bindings.

[Amin Bandali]

[-- Attachment #1: Type: text/plain, Size: 623 bytes --]

Hello!

On 2018-12-21  9:40 PM, Marius Bakke wrote:
> Ludovic Courtès <ludo@gnu.org> writes:
>
>> Hello!
>>
>> [...]
>>
>> Marius, WDYT?
>
> Hello!
>
> I don't actually know z3 at all, I just updated it to fix the build on
> core-updates :-)
>
> In any case dropping python2 bindings seems sensible, seeing as Python 2
> is EOL in a year[1].  So please go ahead, thank you Amin!
>
> [1]: https://www.python.org/dev/peps/pep-0373/
>

Thanks for the reply, Marius.  I’ve attached a new version of the patch
with only Python 3 bindings and with Ludo’s feedback about ‘which’.

Best,
amin


[-- Attachment #2: 0001-gnu-z3-Update-to-4.8.3-and-provide-python3-bindings.patch --]
[-- Type: text/x-patch, Size: 3997 bytes --]

From ed80a156cd0aa3d7839e49bd6ebdd5e2911067ae Mon Sep 17 00:00:00 2001
From: Amin Bandali <bandali@gnu.org>
Date: Fri, 21 Dec 2018 18:27:11 -0500
Subject: [PATCH v2] gnu: z3: Update to 4.8.3 and provide python3 bindings

* gnu/packages/maths.scm (z3): Update to 4.8.3.
[build-system]: Switch from cmake to make, and use the current
scripts/mk_make.py build script instead of the now-deprecated
contrib/cmake/bootstrap.py.
---
 gnu/packages/maths.scm | 32 ++++++++++++++++++++------------
 1 file changed, 20 insertions(+), 12 deletions(-)

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 9fb02b738..f49b50c23 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -29,6 +29,7 @@
 ;;; Copyright © 2018 Marius Bakke <mbakke@fastmail.com>
 ;;; Copyright © 2018 Eric Brown <brown@fastmail.com>
 ;;; Copyright © 2018 Julien Lepiller <julien@lepiller.eu>
+;;; Copyright © 2018 Amin Bandali <bandali@gnu.org>
 ;;;
 ;;; This file is part of GNU Guix.
 ;;;
@@ -116,6 +117,7 @@
   #:use-module (gnu packages tex)
   #:use-module (gnu packages tls)
   #:use-module (gnu packages version-control)
+  #:use-module (gnu packages which)
   #:use-module (gnu packages wxwidgets)
   #:use-module (gnu packages xml)
   #:use-module (srfi srfi-1))
@@ -3965,7 +3967,7 @@ as equations, scalars, vectors, and matrices.")
 (define-public z3
   (package
     (name "z3")
-    (version "4.8.1")
+    (version "4.8.3")
     (home-page "https://github.com/Z3Prover/z3")
     (source (origin
               (method git-fetch)
@@ -3974,16 +3976,10 @@ as equations, scalars, vectors, and matrices.")
               (file-name (git-file-name name version))
               (sha256
                (base32
-                "1vr57bwx40sd5riijyrhy70i2wnv9xrdihf6y5zdz56yq88rl48f"))))
-    (build-system cmake-build-system)
+                "0p5gdmhd32x6zwmx7j5cgwh4jyfxa9yapym95nlmyfaqzak92qar"))))
+    (build-system gnu-build-system)
     (arguments
-     `(#:configure-flags
-       (list "-DBUILD_PYTHON_BINDINGS=true"
-             "-DINSTALL_PYTHON_BINDINGS=true"
-             (string-append "-DCMAKE_INSTALL_PYTHON_PKG_DIR="
-                            %output
-                            "/lib/python2.7/site-packages"))
-       #:phases
+     `(#:phases
        (modify-phases %standard-phases
          (add-after 'unpack 'fix-compatability
            ;; Versions after 4.8.3 have immintrin.h IFDEFed for Windows only.
@@ -3994,7 +3990,18 @@ as equations, scalars, vectors, and matrices.")
          (add-before 'configure 'bootstrap
            (lambda _
              (zero?
-              (system* "python" "contrib/cmake/bootstrap.py" "create"))))
+              (system* "python" "scripts/mk_make.py"))))
+         ;; work around gnu-build-system's setting --enable-fast-install
+         ;; (z3's `configure' is a wrapper around the above python file,
+         ;; which fails when passed --enable-fast-install)
+         (replace 'configure
+           (lambda* (#:key inputs outputs #:allow-other-keys)
+             (invoke "./configure"
+                     (string-append "--prefix=" (assoc-ref outputs "out")))))
+         (add-after 'configure 'change-directory
+           (lambda _
+             (chdir "build")
+             #t))
          (add-before 'check 'make-test-z3
            (lambda _
              ;; Build the test suite executable.
@@ -4005,7 +4012,8 @@ as equations, scalars, vectors, and matrices.")
              ;; Run all the tests that don't require arguments.
              (zero? (system* "./test-z3" "/a")))))))
     (native-inputs
-     `(("python" ,python-2)))
+     `(("which" ,(@ (gnu packages base) which))
+       ("python" ,python-wrapper)))
     (synopsis "Theorem prover")
     (description "Z3 is a theorem prover and @dfn{satisfiability modulo
 theories} (SMT) solver.  It provides a C/C++ API, as well as Python bindings.")
-- 
2.20.1

[bug#33764] [PATCH] gnu: z3: Update to 4.8.3 and add python{, 2}-z3 bindings.

[Amin Bandali]

[-- Attachment #1: Type: text/plain, Size: 163 bytes --]

Apologies, I just realized that I forgot to remove my use of the @
notation in my v2 patch submitted earlier.  I’ve attached an updated one
that doesn’t.


[-- Attachment #2: 0001-gnu-z3-Update-to-4.8.3-and-provide-python3-bindings.patch --]
[-- Type: text/x-patch, Size: 3973 bytes --]

From ad9433c11ebba672db3ca75689ebee92ea9da7de Mon Sep 17 00:00:00 2001
From: Amin Bandali <bandali@gnu.org>
Date: Sat, 22 Dec 2018 10:16:57 -0500
Subject: [PATCH v3] gnu: z3: Update to 4.8.3 and provide python3 bindings

* gnu/packages/maths.scm (z3): Update to 4.8.3.
[build-system]: Switch from cmake to make, and use the current
scripts/mk_make.py build script instead of the now-deprecated
contrib/cmake/bootstrap.py.
---
 gnu/packages/maths.scm | 32 ++++++++++++++++++++------------
 1 file changed, 20 insertions(+), 12 deletions(-)

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 9fb02b738..1b6127e9f 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -29,6 +29,7 @@
 ;;; Copyright © 2018 Marius Bakke <mbakke@fastmail.com>
 ;;; Copyright © 2018 Eric Brown <brown@fastmail.com>
 ;;; Copyright © 2018 Julien Lepiller <julien@lepiller.eu>
+;;; Copyright © 2018 Amin Bandali <bandali@gnu.org>
 ;;;
 ;;; This file is part of GNU Guix.
 ;;;
@@ -116,6 +117,7 @@
   #:use-module (gnu packages tex)
   #:use-module (gnu packages tls)
   #:use-module (gnu packages version-control)
+  #:use-module (gnu packages which)
   #:use-module (gnu packages wxwidgets)
   #:use-module (gnu packages xml)
   #:use-module (srfi srfi-1))
@@ -3965,7 +3967,7 @@ as equations, scalars, vectors, and matrices.")
 (define-public z3
   (package
     (name "z3")
-    (version "4.8.1")
+    (version "4.8.3")
     (home-page "https://github.com/Z3Prover/z3")
     (source (origin
               (method git-fetch)
@@ -3974,16 +3976,10 @@ as equations, scalars, vectors, and matrices.")
               (file-name (git-file-name name version))
               (sha256
                (base32
-                "1vr57bwx40sd5riijyrhy70i2wnv9xrdihf6y5zdz56yq88rl48f"))))
-    (build-system cmake-build-system)
+                "0p5gdmhd32x6zwmx7j5cgwh4jyfxa9yapym95nlmyfaqzak92qar"))))
+    (build-system gnu-build-system)
     (arguments
-     `(#:configure-flags
-       (list "-DBUILD_PYTHON_BINDINGS=true"
-             "-DINSTALL_PYTHON_BINDINGS=true"
-             (string-append "-DCMAKE_INSTALL_PYTHON_PKG_DIR="
-                            %output
-                            "/lib/python2.7/site-packages"))
-       #:phases
+     `(#:phases
        (modify-phases %standard-phases
          (add-after 'unpack 'fix-compatability
            ;; Versions after 4.8.3 have immintrin.h IFDEFed for Windows only.
@@ -3994,7 +3990,18 @@ as equations, scalars, vectors, and matrices.")
          (add-before 'configure 'bootstrap
            (lambda _
              (zero?
-              (system* "python" "contrib/cmake/bootstrap.py" "create"))))
+              (system* "python" "scripts/mk_make.py"))))
+         ;; work around gnu-build-system's setting --enable-fast-install
+         ;; (z3's `configure' is a wrapper around the above python file,
+         ;; which fails when passed --enable-fast-install)
+         (replace 'configure
+           (lambda* (#:key inputs outputs #:allow-other-keys)
+             (invoke "./configure"
+                     (string-append "--prefix=" (assoc-ref outputs "out")))))
+         (add-after 'configure 'change-directory
+           (lambda _
+             (chdir "build")
+             #t))
          (add-before 'check 'make-test-z3
            (lambda _
              ;; Build the test suite executable.
@@ -4005,7 +4012,8 @@ as equations, scalars, vectors, and matrices.")
              ;; Run all the tests that don't require arguments.
              (zero? (system* "./test-z3" "/a")))))))
     (native-inputs
-     `(("python" ,python-2)))
+     `(("which" ,which)
+       ("python" ,python-wrapper)))
     (synopsis "Theorem prover")
     (description "Z3 is a theorem prover and @dfn{satisfiability modulo
 theories} (SMT) solver.  It provides a C/C++ API, as well as Python bindings.")
-- 
2.20.1

bug#33764: [PATCH] gnu: z3: Update to 4.8.3 and add python{, 2}-z3 bindings.

[Ludovic Courtès]

[-- Attachment #1: Type: text/plain, Size: 580 bytes --]

Hi Amin,

Amin Bandali <bandali@gnu.org> skribis:

> From ad9433c11ebba672db3ca75689ebee92ea9da7de Mon Sep 17 00:00:00 2001
> From: Amin Bandali <bandali@gnu.org>
> Date: Sat, 22 Dec 2018 10:16:57 -0500
> Subject: [PATCH v3] gnu: z3: Update to 4.8.3 and provide python3 bindings
>
> * gnu/packages/maths.scm (z3): Update to 4.8.3.
> [build-system]: Switch from cmake to make, and use the current
> scripts/mk_make.py build script instead of the now-deprecated
> contrib/cmake/bootstrap.py.

Applied with the fixes below for ‘which’.

Thank you!

Ludo’.


[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #2: Type: text/x-patch, Size: 1054 bytes --]

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 1b6127e9f7..448d9e373b 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -54,7 +54,7 @@
   #:use-module (guix download)
   #:use-module (guix git-download)
   #:use-module (guix utils)
-  #:use-module (guix build utils)
+  #:use-module ((guix build utils) #:select (alist-replace))
   #:use-module (guix build-system cmake)
   #:use-module (guix build-system gnu)
   #:use-module (guix build-system ocaml)
@@ -64,6 +64,7 @@
   #:use-module (gnu packages algebra)
   #:use-module (gnu packages audio)
   #:use-module (gnu packages autotools)
+  #:use-module (gnu packages base)
   #:use-module (gnu packages bison)
   #:use-module (gnu packages boost)
   #:use-module (gnu packages check)
@@ -117,7 +118,6 @@
   #:use-module (gnu packages tex)
   #:use-module (gnu packages tls)
   #:use-module (gnu packages version-control)
-  #:use-module (gnu packages which)
   #:use-module (gnu packages wxwidgets)
   #:use-module (gnu packages xml)
   #:use-module (srfi srfi-1))