Fix nightly (#7365)

- add some logic to setup.py to handle cross platform tagging correctly
  this adds a dependency on setuptools>=70
- rearrange the nightly CI to use these new builds correctly

Author: rhelmot

scripts/nightly.yaml

@@ -183,7 +183,7 @@ stages:
     - task: CopyFiles@2
       inputs:
         sourceFolder: src/api/python/wheelhouse
-        contents: '*.zip'
+        contents: '*.whl'
         targetFolder: $(Build.ArtifactStagingDirectory)
     - task: PublishPipelineArtifact@0
       inputs:
@@ -209,11 +209,11 @@ stages:
     - script: echo $PATH
     - script: "stat `which aarch64-none-linux-gnu-gcc`"
     - script: "pip install build git+https://github.com./rhelmot/auditwheel"
-    - script: "cd src/api/python && CC=aarch64-none-linux-gnu-gcc CXX=aarch64-none-linux-gnu-g++ AR=aarch64-none-linux-gnu-ar LD=aarch64-none-linux-gnu-ld python -m build && AUDITWHEEL_PLAT= auditwheel repair --best-plat dist/*.whl && cd ../../.."
+    - script: "cd src/api/python && CC=aarch64-none-linux-gnu-gcc CXX=aarch64-none-linux-gnu-g++ AR=aarch64-none-linux-gnu-ar LD=aarch64-none-linux-gnu-ld Z3_CROSS_COMPILING=aarch64 python -m build && AUDITWHEEL_PLAT= auditwheel repair --best-plat dist/*.whl && cd ../../.."
     - task: CopyFiles@2
       inputs:
         sourceFolder: src/api/python/wheelhouse
-        contents: '*.zip'
+        contents: '*.whl'
         targetFolder: $(Build.ArtifactStagingDirectory)
     - task: PublishPipelineArtifact@0
       inputs:
@@ -504,21 +504,18 @@ stages:
         targetPath: $(Agent.TempDirectory)
     - script: cd $(Agent.TempDirectory); mkdir osx-x64-bin; cd osx-x64-bin; unzip ../*x64-osx*.zip
     - script: cd $(Agent.TempDirectory); mkdir osx-arm64-bin; cd osx-arm64-bin; unzip ../*arm64-osx*.zip
-    - script: cd $(Agent.TempDirectory); mkdir libc-x64-bin; cd libc-x64-bin; unzip ../*x64-glibc*.zip
-    - script: cd $(Agent.TempDirectory); mkdir libc-arm64-bin; cd libc-arm64-bin; unzip ../*arm64-glibc*.zip
 #    - script: cd $(Agent.TempDirectory); mkdir musl-bin; cd musl-bin; unzip ../*-linux.zip
     - script: cd $(Agent.TempDirectory); mkdir win32-bin; cd win32-bin; unzip ../*x86-win*.zip
     - script: cd $(Agent.TempDirectory); mkdir win64-bin; cd win64-bin; unzip ../*x64-win*.zip
-    - script: python3 -m pip install --user -U setuptools wheel
+    - script: python3 -m pip install --user -U setuptools
     - script: cd src/api/python; python3 setup.py sdist
     # take a look at this PREMIUM HACK I came up with to get around the fact that the azure variable syntax overloads the bash syntax for subshells
-    - script: cd src/api/python; echo $(Agent.TempDirectory)/libc-x64-bin/* | xargs printf 'PACKAGE_FROM_RELEASE=%s\n' | xargs -I '{}' env '{}' python3 setup.py bdist_wheel
-    - script: cd src/api/python; echo $(Agent.TempDirectory)/libc-arm64-bin/* | xargs printf 'PACKAGE_FROM_RELEASE=%s\n' | xargs -I '{}' env '{}' python3 setup.py bdist_wheel
 #   - script: cd src/api/python; echo $(Agent.TempDirectory)/musl-bin/* | xargs printf 'PACKAGE_FROM_RELEASE=%s\n' | xargs -I '{}' env '{}' python3 setup.py bdist_wheel
     - script: cd src/api/python; echo $(Agent.TempDirectory)/win32-bin/* | xargs printf 'PACKAGE_FROM_RELEASE=%s\n' | xargs -I '{}' env '{}' python3 setup.py bdist_wheel
     - script: cd src/api/python; echo $(Agent.TempDirectory)/win64-bin/* | xargs printf 'PACKAGE_FROM_RELEASE=%s\n' | xargs -I '{}' env '{}' python3 setup.py bdist_wheel
     - script: cd src/api/python; echo $(Agent.TempDirectory)/osx-x64-bin/* | xargs printf 'PACKAGE_FROM_RELEASE=%s\n' | xargs -I '{}' env '{}' python3 setup.py bdist_wheel
     - script: cd src/api/python; echo $(Agent.TempDirectory)/osx-arm64-bin/* | xargs printf 'PACKAGE_FROM_RELEASE=%s\n' | xargs -I '{}' env '{}' python3 setup.py bdist_wheel
+    - script: cp $(Agent.TempDirectory)/*.whl src/api/python/dist
     - task: PublishPipelineArtifact@0
       inputs:
         artifactName: 'Python packages'

src/api/python/pyproject.toml

@@ -1,3 +1,3 @@
 [build-system]
-requires = ["setuptools>=59", "wheel", "cmake"]
+requires = ["setuptools>=70", "cmake"]
 build-backend = "setuptools.build_meta"

src/api/python/setup.py

@@ -9,6 +9,7 @@
 from setuptools import setup
 from setuptools.command.build import build as _build
 from setuptools.command.sdist import sdist as _sdist
+from setuptools.command.bdist_wheel import bdist_wheel as _bdist_wheel
 from setuptools.command.develop import develop as _develop
 
 class LibError(Exception):
@@ -31,6 +32,8 @@ class LibError(Exception):
     HEADER_DIRS = [os.path.join(SRC_DIR, 'src', 'api'), os.path.join(SRC_DIR, 'src', 'api', 'c++')]
     RELEASE_METADATA = None
     BUILD_PLATFORM = sys.platform
+    BUILD_ARCH = os.environ.get("Z3_CROSS_COMPILING", platform.machine())
+    BUILD_OS_VERSION = platform.mac_ver()[0].split(".")
 else:
     if not os.path.isdir(RELEASE_DIR):
         raise Exception("RELEASE_DIR (%s) is not a directory!" % RELEASE_DIR)
@@ -41,6 +44,11 @@ class LibError(Exception):
         raise Exception("RELEASE_DIR (%s) must be in the format z3-version-arch-os[-osversion] so we can extract metadata from it. Sorry!" % RELEASE_DIR)
     RELEASE_METADATA.pop(0)
     BUILD_PLATFORM = RELEASE_METADATA[2]
+    BUILD_ARCH = RELEASE_METADATA[1]
+    if len(RELEASE_METADATA) == 4:
+        BUILD_OS_VERSION = RELEASE_METADATA[3].split(".")
+    else:
+        BUILD_OS_VERSION = None
 
 # determine where destinations are
 LIBS_DIR = os.path.join(ROOT_DIR, 'z3', 'lib')
@@ -242,21 +250,29 @@ def run(self):
         self.execute(_copy_sources, (), msg="Copying source files")
         _sdist.run(self)
 
-# platform.freedesktop_os_release was added in 3.10
-os_id = ''
-if hasattr(platform, 'freedesktop_os_release'):
-    try:
-        osr = platform.freedesktop_os_release()
-        print(osr)
-        os_id = osr['ID']
-    except OSError:
-        pass
+class bdist_wheel(_bdist_wheel):
+    def finalize_options(self):
+        if BUILD_ARCH is not None and BUILD_PLATFORM is not None:
+            os_version_tag = '_'.join(BUILD_OS_VERSION[:2]) if BUILD_OS_VERSION is not None else 'xxxxxx'
+            TAGS = {
+                # linux tags cannot be deployed - they must be auditwheel'd to pick the right compatibility tag based on imported libc symbol versions
+                ("linux", "x86_64"): "linux_x86_64",
+                ("linux", "aarch64"): "linux_aarch64",
+                # windows arm64 is not supported by pypi yet
+                ("win", "x64"): "win_amd64",
+                ("win", "x86"): "win32",
+                ("osx", "x64"): f"macosx_{os_version_tag}_x86_64",
+                ("osx", "arm64"): f"macosx_{os_version_tag}_arm64",
+            }  # type: dict[tuple[str, str], str]
+            self.plat_name = TAGS[(BUILD_PLATFORM, BUILD_ARCH)]
+        return super().finalize_options()
+
 
 setup(
     name='z3-solver',
     version=_z3_version(),
     description='an efficient SMT solver library',
-    long_description='Z3 is a theorem prover from Microsoft Research with support for bitvectors, booleans, arrays, floating point numbers, strings, and other data types.\n\nFor documentation, please read http://z3prover.github.io/api/html/z3.html\n\nIn the event of technical difficulties related to configuration, compilation, or installation, please submit issues to https://github.com./z3prover/z3.git',
+    long_description='Z3 is a theorem prover from Microsoft Research with support for bitvectors, booleans, arrays, floating point numbers, strings, and other data types.\n\nFor documentation, please read http://z3prover.github.io/api/html/z3.html',
     author="The Z3 Theorem Prover Project",
     maintainer="Audrey Dutcher and Nikolaj Bjorner",
     maintainer_email="[email protected]",
@@ -270,5 +286,5 @@ def run(self):
         'z3': [os.path.join('lib', '*'), os.path.join('include', '*.h'), os.path.join('include', 'c++', '*.h')]
     },
     data_files=[('bin',[os.path.join('bin',EXECUTABLE_FILE)])],
-    cmdclass={'build': build, 'develop': develop, 'sdist': sdist},
+    cmdclass={'build': build, 'develop': develop, 'sdist': sdist, 'bdist_wheel': bdist_wheel},
 )