[bug#27461] [PATCH v2 2/2] gnu: Add python2-z3.

[ludo@gnu.org (Ludovic Courtès)]

Hi,

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

> From: Julien Lepiller <julien@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’.