search

Z3Prover / z3

The Z3 Theorem Prover
Other
9.96k stars 1.46k forks source link

aarch64 linux wheel is tagged `manylinux2014` despite actually being `manylinux_2_34` #7232

Open burgholzer opened 1 month ago

burgholzer commented 1 month ago

As other issues have already pointed out, the aarch64 linux wheel is actually an x86_64 wheel that is incorrectly tagged. (related issue #7201). However, there is an even more severe issue with the Python wheels of Z3:

Running

auditwheel show z3_solver-4.13.0.0-py2.py3-none-manylinux2014_aarch64.whl

reveals

z3_solver-4.13.0.0-py2.py3-none-manylinux2014_aarch64.whl is
consistent with the following platform tag: "manylinux_2_34_x86_64".

The wheel references external versioned symbols in these
system-provided shared libraries: libgcc_s.so.1 with versions
{'GCC_3.0'}, libm.so.6 with versions {'GLIBC_2.29', 'GLIBC_2.17'},
libc.so.6 with versions {'GLIBC_2.34', 'GLIBC_2.32', 'GLIBC_2.17',
'GLIBC_2.33'}, libstdc++.so.6 with versions {'GLIBCXX_3.4.21',
'CXXABI_1.3.9', 'GLIBCXX_3.4.17', 'GLIBCXX_3.4.20', 'GLIBCXX_3.4.15',
'GLIBCXX_3.4.29', 'GLIBCXX_3.4.19', 'GLIBCXX_3.4.22',
'GLIBCXX_3.4.26', 'CXXABI_1.3.2', 'GLIBCXX_3.4', 'GLIBCXX_3.4.11',
'CXXABI_1.3', 'GLIBCXX_3.4.9', 'GLIBCXX_3.4.18', 'GLIBCXX_3.4.14'}

This constrains the platform tag to "manylinux_2_34_x86_64". In order
to achieve a more compatible tag, you would need to recompile a new
wheel from source on a system with earlier versions of these
libraries, such as a recent manylinux image.

This implies that the corresponding wheel uses symbols that are way newer than manylinux2014. Notably, this trips up auditwheel repair steps in depending projects because auditwheel (correctly) determines that the resulting wheel cannot be manylinux2014 tagged (which corresponds to manylinux_2_17). See https://github.com/cda-tum/mqt-qmap/actions/runs/9207479206/job/25327747246?pr=456#step:5:612 for an example failure. While manylinux2014 will reach end of life soon, the next step after that seems to be manylinux_2_28, which is still way older than manylinux_2_34 used for the aarch64 wheels here.

Given the incorrect tagging, I think the respective wheel should be yanked from PyPI. It can only create problems for people using it. Furthermore: Is there any reason for not creating a proper manylinux2014 tagged aarch64 wheel similar to the x86_64 wheel (which only contains proper symbols according to auditwheel).