[bug#33764] gnu: z3: Update to 4.8.3 and add python{, 2}-z3 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/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(-)

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

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.

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

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

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/