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

Previous Next

To add a comment to this bug, you must first unarchive it, by sending
a message to control AT debbugs.gnu.org, with unarchive 33764 in the body.
You can then email your comments to 33764 AT debbugs.gnu.org in the normal way.

Toggle the display of automated, internal messages from the tracker.

Message #5 received at submit <at> debbugs.gnu.org (full text, mbox):

From: Amin Bandali <bandali <at> gnu.org>
To: guix-patches <at> gnu.org
Cc: Amin Bandali <bandali <at> gnu.org>
Subject: [PATCH] gnu: z3: Update to 4.8.3 and add python{,2}-z3 bindings.
Date: Sat, 15 Dec 2018 23:05:30 -0500

* 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 <at> fastmail.com>
 ;;; Copyright © 2018 Eric Brown <brown <at> fastmail.com>
 ;;; Copyright © 2018 Julien Lepiller <julien <at> lepiller.eu>
+;;; Copyright © 2018 Amin Bandali <bandali <at> 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 <at> lassieur.org>
 ;;; Copyright © 2018 Maxim Cournoyer <maxim.cournoyer <at> gmail.com>
 ;;; Copyright © 2018 Luther Thompson <lutheroto <at> gmail.com>
+;;; Copyright © 2018 Amin Bandali <bandali <at> 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

Message #8 received at 33764 <at> debbugs.gnu.org (full text, mbox):

From: Ludovic Courtès <ludo <at> gnu.org>
To: Amin Bandali <bandali <at> gnu.org>
Cc: 33764 <at> debbugs.gnu.org
Subject: Re: [bug#33764] [PATCH] gnu: z3: Update to 4.8.3 and add python{,
 2}-z3 bindings.
Date: Sun, 16 Dec 2018 16:18:16 +0100

Hello Amin,

Amin Bandali <bandali <at> 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 <at> lassieur.org>
>  ;;; Copyright © 2018 Maxim Cournoyer <maxim.cournoyer <at> gmail.com>
>  ;;; Copyright © 2018 Luther Thompson <lutheroto <at> gmail.com>
> +;;; Copyright © 2018 Amin Bandali <bandali <at> 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’.

Message #11 received at 33764 <at> debbugs.gnu.org (full text, mbox):

From: Efraim Flashner <efraim <at> flashner.co.il>
To: Ludovic Courtès <ludo <at> gnu.org>
Cc: 33764 <at> debbugs.gnu.org, Amin Bandali <bandali <at> gnu.org>
Subject: Re: [bug#33764] [PATCH] gnu: z3: Update to 4.8.3 and add python{,
 2}-z3 bindings.
Date: Mon, 17 Dec 2018 09:29:21 +0200

[Message part 1 (text/plain, inline)]

On Sun, Dec 16, 2018 at 04:18:16PM +0100, Ludovic Courtès wrote:
> Hello Amin,
> 
> Amin Bandali <bandali <at> 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 <at> lassieur.org>
> >  ;;; Copyright © 2018 Maxim Cournoyer <maxim.cournoyer <at> gmail.com>
> >  ;;; Copyright © 2018 Luther Thompson <lutheroto <at> gmail.com>
> > +;;; Copyright © 2018 Amin Bandali <bandali <at> 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 <at> 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

[signature.asc (application/pgp-signature, inline)]

Message #14 received at 33764 <at> debbugs.gnu.org (full text, mbox):

From: Amin Bandali <bandali <at> gnu.org>
To: Efraim Flashner <efraim <at> flashner.co.il>
Cc: Ludovic Courtès <ludo <at> gnu.org>, 33764 <at> debbugs.gnu.org,
 Marius Bakke <mbakke <at> fastmail.com>
Subject: Re: [bug#33764] [PATCH] gnu: z3: Update to 4.8.3 and add python{,
 2}-z3 bindings.
Date: Mon, 17 Dec 2018 09:34:11 -0500

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

Message #17 received at 33764 <at> debbugs.gnu.org (full text, mbox):

From: Ludovic Courtès <ludo <at> gnu.org>
To: Amin Bandali <bandali <at> gnu.org>
Cc: Marius Bakke <mbakke <at> fastmail.com>, 33764 <at> debbugs.gnu.org,
 Efraim Flashner <efraim <at> flashner.co.il>
Subject: Re: [bug#33764] [PATCH] gnu: z3: Update to 4.8.3 and add python{,
 2}-z3 bindings.
Date: Fri, 21 Dec 2018 18:02:02 +0100

Hello!

Amin Bandali <bandali <at> 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’.

Message #20 received at 33764 <at> debbugs.gnu.org (full text, mbox):

From: Marius Bakke <mbakke <at> fastmail.com>
To: Ludovic Courtès <ludo <at> gnu.org>, Amin Bandali
 <bandali <at> gnu.org>
Cc: 33764 <at> debbugs.gnu.org, Efraim Flashner <efraim <at> flashner.co.il>
Subject: Re: [bug#33764] [PATCH] gnu: z3: Update to 4.8.3 and add python{,
 2}-z3 bindings.
Date: Fri, 21 Dec 2018 21:40:47 +0100

[Message part 1 (text/plain, inline)]

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

> Hello!
>
> Amin Bandali <bandali <at> 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/

[signature.asc (application/pgp-signature, inline)]

Message #23 received at 33764 <at> debbugs.gnu.org (full text, mbox):

From: Amin Bandali <bandali <at> gnu.org>
To: Marius Bakke <mbakke <at> fastmail.com>
Cc: Ludovic Courtès <ludo <at> gnu.org>, 33764 <at> debbugs.gnu.org,
 Efraim Flashner <efraim <at> flashner.co.il>
Subject: Re: [bug#33764] [PATCH] gnu: z3: Update to 4.8.3 and add python{,
 2}-z3 bindings.
Date: Fri, 21 Dec 2018 18:41:51 -0500

[Message part 1 (text/plain, inline)]

Hello!

On 2018-12-21  9:40 PM, Marius Bakke wrote:
> Ludovic Courtès <ludo <at> 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

[0001-gnu-z3-Update-to-4.8.3-and-provide-python3-bindings.patch (text/x-patch, attachment)]

Message #26 received at 33764 <at> debbugs.gnu.org (full text, mbox):

From: Amin Bandali <bandali <at> gnu.org>
To: Marius Bakke <mbakke <at> fastmail.com>
Cc: Ludovic Courtès <ludo <at> gnu.org>, 33764 <at> debbugs.gnu.org,
 Efraim Flashner <efraim <at> flashner.co.il>
Subject: Re: [bug#33764] [PATCH] gnu: z3: Update to 4.8.3 and add python{,
 2}-z3 bindings.
Date: Sat, 22 Dec 2018 10:20:55 -0500

[Message part 1 (text/plain, inline)]

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.

[0001-gnu-z3-Update-to-4.8.3-and-provide-python3-bindings.patch (text/x-patch, attachment)]

Message #31 received at 33764-done <at> debbugs.gnu.org (full text, mbox):

From: Ludovic Courtès <ludo <at> gnu.org>
To: Amin Bandali <bandali <at> gnu.org>
Cc: Marius Bakke <mbakke <at> fastmail.com>, 33764-done <at> debbugs.gnu.org,
 Efraim Flashner <efraim <at> flashner.co.il>
Subject: Re: [bug#33764] [PATCH] gnu: z3: Update to 4.8.3 and add python{,
 2}-z3 bindings.
Date: Sun, 23 Dec 2018 18:33:59 +0100

[Message part 1 (text/plain, inline)]

Hi Amin,

Amin Bandali <bandali <at> gnu.org> skribis:

> From ad9433c11ebba672db3ca75689ebee92ea9da7de Mon Sep 17 00:00:00 2001
> From: Amin Bandali <bandali <at> 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’.

[Message part 2 (text/x-patch, inline)]

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

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.