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

Previous Next

Package: guix-patches;

Reported by: Amin Bandali <bandali <at> gnu.org>

Date: Sun, 16 Dec 2018 04:37:01 UTC

Severity: normal

Tags: patch

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

Bug is archived. No further changes may be made.

Full log


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




This bug report was last modified 6 years and 233 days ago.

Previous Next


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