[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