GNU bug report logs - #27461
[PATCH] gnu: Add z3.

Previous Next

Full log

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

From: ludo <at> gnu.org (Ludovic Courtès)
To: Theodoros Foradis <theodoros.for <at> openmailbox.org>
Cc: julien <at> lepiller.eu, 27461 <at> debbugs.gnu.org
Subject: Re: [bug#27461] [PATCH v2 2/2] gnu: Add python2-z3.
Date: Sat, 29 Jul 2017 23:03:14 +0200

Hi,

Theodoros Foradis <theodoros.for <at> openmailbox.org> skribis:

> From: Julien Lepiller <julien <at> lepiller.eu>
>
> * gnu/packages/python.scm (python2-z3): New variable.

[...]

> +(define-public python2-z3
> +  (package
> +    (inherit z3)
> +    (name "python2-z3")

Please add (synopsis "Python bindings to the Z3 theorem prover").

> +    (build-system python-build-system)
> +    (propagated-inputs
> +     `(("z3" ,z3)))

Can we avoid propagating it?

> +     (arguments
> +      `(#:python ,python-2
> +        #:phases
> +        (modify-phases %standard-phases
> +          (add-before 'build 'prepare
> +            (lambda* (#:key inputs #:allow-other-keys)

It would be nice to have comments in this procedure to help understand
what’s going on.

> +              (system* "python" "scripts/mk_make.py")
> +              (copy-file "build/python/z3/z3core.py"
> +                         "src/api/python/z3/z3core.py")
> +              (copy-file "build/python/z3/z3consts.py"
> +                         "src/api/python/z3/z3consts.py")

You can use (install-file "build/python/z3/z3consts.py" "src/api/python/z3").

> +              (chdir "src/api/python")
> +              (substitute* "z3/z3core.py"
> +                (("_dirs = \\[")
> +                 (string-append "_dirs = ['" (assoc-ref inputs "z3")
> +                                "/lib', ")))
> +              (substitute* "MANIFEST.in"
> +                ((".*") ""))
> +              (substitute* "setup.py"
> +                (("self.execute\\(.*") "\n")
> +                (("scripts=.*") "\n"))
> +              #t)))))))

Also, since Z3 already depends on Python, would it make sense to have a
single package?

Thanks,
Ludo’.

Previous Next

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