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

["Ludovic Courtès" <ludo@gnu.org>]

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