Recent OSX wheels cannot be installed on Intel

[stessaris]

The OSX wheels built for intel, starting from release z3-4.12.3, use the tag name macosx_11_7 which is not recognised by pip as compatible with more recent OSX versions. This can be verified looking at the output from pip debug --verbose under the Compatible tags section.

Apparently, from 11 on, the minor should be always 0 (see the output of pip debug --verbose|grep 'macosx_1[1-9]_[^0]'). I tested this on an intel macbook with Ventura 13.6.1 (the only mac box I have access to) with different Python versions.

I noticed that the arm version is correctly tagged macosx_11_0, and z3-4.12.2 was the last release with a wheel with a 10_x tag (was macosx_10_16_x86_64, among the compatible ones).

If the wheel file is renamed by changing _7_ to _0_, then it can be installed via pip.

[stessaris]

I looked at the way pip is checking for compatibility for the tags, and there's no way a tag with _1[1,-9]_[^0] (i.e., with a non-zero minor) will be accepted as compatible. For reference, see the discussion in pypa/packaging#578 and the code that generates the compatible tags in pypa/pip/src/pip/_vendor/packaging/tags.py#L377.

As a workaround, I suggest renaming the wheel before creating the release and uploading to pypi

[NikolajBjorner]

This must be a regression, maybe due to newer versions of MacOS on the build machines.
The build machines use a "fake" macos version. It is the one you see.
Pip packaging should have corrected it.

[NikolajBjorner]

6cd619d

[NikolajBjorner]

Could you dry-run the nigthly? https://github.com/Z3Prover/z3/releases/tag/Nightly

[stessaris]

The nightly release installs just fine:

(z3) $ pip install https://github.com/Z3Prover/z3/releases/download/Nightly/z3_solver-4.12.5.0-py2.py3-none-macosx_11_0_x86_64.whl
Collecting z3-solver==4.12.5.0
  Using cached https://github.com/Z3Prover/z3/releases/download/Nightly/z3_solver-4.12.5.0-py2.py3-none-macosx_11_0_x86_64.whl (63.5 MB)
Collecting importlib-resources (from z3-solver==4.12.5.0)
  Using cached importlib_resources-6.1.1-py3-none-any.whl.metadata (4.1 kB)
Using cached importlib_resources-6.1.1-py3-none-any.whl (33 kB)
Installing collected packages: importlib-resources, z3-solver
Successfully installed importlib-resources-6.1.1 z3-solver-4.12.5.0
(z3) $ pip list
Package             Version
------------------- --------
importlib-resources 6.1.1
pip                 23.3.1
setuptools          68.2.2
wheel               0.42.0
z3-solver           4.12.5.0

May I suggest substituting the added lines added in 6cd619d with something along:

plat_name ='macosx_%s_x86_64' % re.sub(r'\A(1[1-9])(_[\d]+)*\Z', r'\1_0', osver.replace('.', '_'))

in the lines 319 and 321? In this way you'll also cover the next releases (e.g. I'm running in 13.6.1), and you don't modify osver, which might be handy in case that you get the exception from line 323.

Note that discussion on pypa/packaging#578 resumed, because ignoring minor versions could be problematic. So, in the future you might want to go back on major/minor tag names.

BTW with Z3 you're doing an outstanding work; I mainly use it to teach computational logic and it's one of the most accessible state of the art tools out there

[NikolajBjorner]

the new release uses the 11_0 naming scheme

[coreycerovsek]

Hi! There's a regression from 4.13.1 whereby x86_64 wheels have reverted to the naming scheme with non-zero minor version numbers. That causes pip to ignore those wheels and fall back to trying to install from source, which fails in turn for me because the tuple ('darwin', 'x86_64') isn't in finalize_options in setup.py. In the Azure pipelines, vmImage was updated to macOS-latest in 8d831a, but only the MacBuildArm64 job passes --os=osx-11.0 to mk_unix_dist.py.