Re: [Buildroot] [PATCH next 1/1] package/z3: new package

["Yann E. MORIN" <yann.morin.1998@free.fr>]

Julien, All,

On 2022-11-19 13:05 +0100, Julien Olivain spake thusly:
> Z3, also known as the Z3 Theorem Prover, is a cross-platform
> satisfiability modulo theories (SMT) solver.
> 
> https://github.com/Z3Prover/z3
> 
> Signed-off-by: Julien Olivain <ju.o@free.fr>
[--SNIP--]
> diff --git a/package/z3/Config.in b/package/z3/Config.in
> new file mode 100644
> index 0000000000..a3f57f7f88
> --- /dev/null
> +++ b/package/z3/Config.in
> @@ -0,0 +1,23 @@
> +config BR2_PACKAGE_Z3
> +	bool "z3"
> +	depends on BR2_INSTALL_LIBSTDCPP
> +	depends on BR2_TOOLCHAIN_GCC_AT_LEAST_7 # c++17
> +	# z3 needs fenv.h which is not provided by uclibc
> +	depends on !BR2_TOOLCHAIN_USES_UCLIBC
> +	# fenv.h lacks FE_INVALID, FE_OVERFLOW & FE_UNDERFLOW on nios2
> +	depends on !BR2_nios2
> +	help
> +	  Z3, also known as the Z3 Theorem Prover, is a cross-platform
> +	  satisfiability modulo theories (SMT) solver.
> +
> +	  https://github.com/Z3Prover/z3
> +
> +if BR2_PACKAGE_Z3
> +
> +config BR2_PACKAGE_Z3_PYTHON
> +	bool "Python bindings"
> +	select BR2_PACKAGE_PYTHON3 # runtime

To me, it makes more sense that python bindings depend on python being
enabled, rather than forcing it. Indeed, if the python is not enabled
(either manually or because it is not selected by an application), then
there is no reason to enable it just to provide bindings.

And we do have that construct in at least a few other packages that
provide python bindings: libftdi1, libiio, ola... So I changed it to
match.  (yes, there are other packages that use select, but that's not a
reason to do things better nowadays! ;-) )

[--SNIP--]
> diff --git a/support/testing/tests/package/test_z3/rootfs-overlay/root/z3test.py b/support/testing/tests/package/test_z3/rootfs-overlay/root/z3test.py
> new file mode 100755
> index 0000000000..6ac53b98c5
> --- /dev/null
> +++ b/support/testing/tests/package/test_z3/rootfs-overlay/root/z3test.py
> @@ -0,0 +1,21 @@
> +#! /usr/bin/env python3
> +
> +from z3 import *

Not all of check-package/flake8 tests are run against files in the
runtime test-suite, but I have a hook that does it, and it reports:

    WARNING: support/testing/tests/package/test_z3/rootfs-overlay/root/z3test.py:3:1: F403 'from z3 import *' used; unable to detect undefined names
    WARNING: support/testing/tests/package/test_z3/rootfs-overlay/root/z3test.py:5:5: F405 'Real' may be undefined, or defined from star imports: z3
    WARNING: support/testing/tests/package/test_z3/rootfs-overlay/root/z3test.py:6:5: F405 'Real' may be undefined, or defined from star imports: z3
    WARNING: support/testing/tests/package/test_z3/rootfs-overlay/root/z3test.py:7:5: F405 'Real' may be undefined, or defined from star imports: z3
    WARNING: support/testing/tests/package/test_z3/rootfs-overlay/root/z3test.py:8:5: F405 'Solver' may be undefined, or defined from star imports: z3
    WARNING: support/testing/tests/package/test_z3/rootfs-overlay/root/z3test.py:20:17: F405 'sat' may be undefined, or defined from star imports: z3
    WARNING: 1     F403 'from z3 import *' used; unable to detect undefined names
    WARNING: 5     F405 'Real' may be undefined, or defined from star imports: z3

So I changed the test to import the whole z3 module, and to prefix
objects with z3.:

    x = z3.Real('x')

and so on...

Applied to next, thanks.

Regards,
Yann E. MORIN.

-- 
.-----------------.--------------------.------------------.--------------------.
|  Yann E. MORIN  | Real-Time Embedded | /"\ ASCII RIBBON | Erics' conspiracy: |
| +33 662 376 056 | Software  Designer | \ / CAMPAIGN     |  ___               |
| +33 561 099 427 `------------.-------:  X  AGAINST      |  \e/  There is no  |
| http://ymorin.is-a-geek.org/ | _/*\_ | / \ HTML MAIL    |   v   conspiracy.  |
'------------------------------^-------^------------------^--------------------'
_______________________________________________
buildroot mailing list
buildroot@buildroot.org
https://lists.buildroot.org/mailman/listinfo/buildroot