diff --git a/src/api/python/demonstrate_fix.py b/src/api/python/demonstrate_fix.py new file mode 100755 index 000000000..bc2ca19bf --- /dev/null +++ b/src/api/python/demonstrate_fix.py @@ -0,0 +1,140 @@ +#!/usr/bin/env python3 +""" +Demonstration script showing that the dist-info fix works. +This script validates that z3-solver can be detected by downstream packages. +""" + +import subprocess +import sys +import tempfile +import os +from pathlib import Path + +def demonstrate_fix(): + """Demonstrate that the fix allows proper package detection.""" + print("=" * 60) + print("Demonstrating z3-solver dist-info fix") + print("=" * 60) + + # Show that the package is properly installed with dist-info + try: + import importlib.metadata as metadata + dist = metadata.distribution('z3-solver') + print(f"✓ Package detectable: {dist.name} v{dist.version}") + print(f" Location: {dist.locate_file('.')}") + print(f" Has {len(list(dist.files)) if dist.files else 0} files") + except metadata.PackageNotFoundError: + print("✗ Package not found by importlib.metadata") + return False + + # Test pip detection + result = subprocess.run([sys.executable, '-m', 'pip', 'show', 'z3-solver'], + capture_output=True, text=True) + if result.returncode == 0: + print("✓ Package detectable by pip show") + for line in result.stdout.split('\n'): + if line.startswith(('Name:', 'Version:', 'Location:')): + print(f" {line}") + else: + print("✗ Package not detectable by pip show") + return False + + # Find the actual dist-info directory + import site + site_packages_dirs = site.getsitepackages() + if hasattr(site, 'getusersitepackages'): + site_packages_dirs.append(site.getusersitepackages()) + + # Also check current environment + try: + import z3 + z3_path = Path(z3.__file__).parent.parent + site_packages_dirs.append(str(z3_path)) + except ImportError: + pass + + dist_info_found = False + for site_dir in site_packages_dirs: + site_path = Path(site_dir) + if site_path.exists(): + dist_info_dirs = list(site_path.glob("z3_solver*.dist-info")) + if dist_info_dirs: + dist_info_dir = dist_info_dirs[0] + print(f"✓ Found dist-info directory: {dist_info_dir}") + + # Check contents + metadata_file = dist_info_dir / "METADATA" + if metadata_file.exists(): + print(f"✓ METADATA file exists: {metadata_file}") + with open(metadata_file) as f: + content = f.read() + if "Name: z3-solver" in content: + print("✓ METADATA contains correct package name") + else: + print("✗ METADATA missing correct package name") + return False + else: + print("✗ METADATA file missing") + return False + + # List all files in dist-info + print(" dist-info contents:") + for item in sorted(dist_info_dir.iterdir()): + print(f" {item.name}") + + dist_info_found = True + break + + if not dist_info_found: + print("✗ No dist-info directory found") + return False + + # Simulate what a downstream package would do + print("\n" + "=" * 60) + print("Simulating downstream package detection") + print("=" * 60) + + downstream_check = ''' +import sys +try: + import pkg_resources + try: + pkg_resources.get_distribution("z3-solver") + print("✓ pkg_resources can find z3-solver") + except pkg_resources.DistributionNotFound: + print("✗ pkg_resources cannot find z3-solver") + sys.exit(1) + + import importlib.metadata as metadata + try: + metadata.distribution("z3-solver") + print("✓ importlib.metadata can find z3-solver") + except metadata.PackageNotFoundError: + print("✗ importlib.metadata cannot find z3-solver") + sys.exit(1) + + print("✓ All downstream detection methods work!") + +except Exception as e: + print(f"✗ Error in downstream detection: {e}") + sys.exit(1) +''' + + result = subprocess.run([sys.executable, '-c', downstream_check], + capture_output=True, text=True) + if result.returncode == 0: + print(result.stdout.strip()) + else: + print("✗ Downstream detection failed:") + print(result.stderr.strip()) + return False + + print("\n" + "=" * 60) + print("SUCCESS: z3-solver dist-info fix is working correctly!") + print("Downstream packages can now detect z3-solver installation.") + print("=" * 60) + return True + +if __name__ == "__main__": + success = demonstrate_fix() + sys.exit(0 if success else 1) \ No newline at end of file diff --git a/src/api/python/pyproject.toml b/src/api/python/pyproject.toml index 380744c87..54c401c28 100644 --- a/src/api/python/pyproject.toml +++ b/src/api/python/pyproject.toml @@ -1,3 +1,54 @@ [build-system] requires = ["setuptools>=70"] build-backend = "setuptools.build_meta" + +[project] +name = "z3-solver" +dynamic = ["version"] +description = "an efficient SMT solver library" +readme = "README.txt" +requires-python = ">=3.8" +license = {text = "MIT"} +authors = [ + {name = "The Z3 Theorem Prover Project"} +] +maintainers = [ + {name = "Audrey Dutcher and Nikolaj Bjorner", email = "audrey@rhelmot.io"} +] +keywords = ["z3", "smt", "sat", "prover", "theorem"] +classifiers = [ + "Development Status :: 5 - Production/Stable", + "Intended Audience :: Developers", + "Intended Audience :: Science/Research", + "Operating System :: OS Independent", + "Programming Language :: Python :: 3", + "Programming Language :: Python :: 3.8", + "Programming Language :: Python :: 3.9", + "Programming Language :: Python :: 3.10", + "Programming Language :: Python :: 3.11", + "Programming Language :: Python :: 3.12", + "Topic :: Scientific/Engineering", + "Topic :: Scientific/Engineering :: Mathematics", + "Topic :: Software Development :: Libraries :: Python Modules", +] +dependencies = [ + "importlib-resources; python_version < '3.9'" +] + +[project.urls] +Homepage = "https://github.com/Z3Prover/z3" +"Bug Reports" = "https://github.com/Z3Prover/z3/issues" +Repository = "https://github.com/Z3Prover/z3" +Documentation = "http://z3prover.github.io/api/html/z3.html" + +[tool.setuptools] +packages = ["z3"] +include-package-data = true + +[tool.setuptools.package-data] +z3 = ["lib/*", "include/*.h", "include/c++/*.h"] + +[tool.setuptools.data-files] +bin = ["bin/*"] + + diff --git a/src/api/python/setup.py b/src/api/python/setup.py index 4d26367b3..c6fdf7205 100644 --- a/src/api/python/setup.py +++ b/src/api/python/setup.py @@ -9,7 +9,11 @@ import glob 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 +try: + from wheel.bdist_wheel import bdist_wheel as _bdist_wheel +except ImportError: + # wheel package not available, provide a dummy class + from setuptools.command.build import build as _bdist_wheel from setuptools.command.develop import develop as _develop class LibError(Exception): @@ -112,6 +116,7 @@ def _clean_native_build(): rmtree(BUILD_DIR) def _z3_version(): + # Get version from project metadata post = os.getenv('Z3_VERSION_SUFFIX', '') if RELEASE_DIR is None: fn = os.path.join(SRC_DIR, 'scripts', 'mk_project.py') @@ -284,7 +289,7 @@ class sdist(_sdist): # The Azure Dev Ops pipelines use internal OS version tagging that don't correspond # to releases. -internal_build_re = re.compile("(.+)\_7") +internal_build_re = re.compile(r"(.+)\_7") class bdist_wheel(_bdist_wheel): @@ -323,19 +328,10 @@ class bdist_wheel(_bdist_wheel): setup( - name='z3-solver', + # Most configuration is now in pyproject.toml + # Keep only setup.py-specific configuration 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', - author="The Z3 Theorem Prover Project", - maintainer="Audrey Dutcher and Nikolaj Bjorner", - maintainer_email="audrey@rhelmot.io", - url='https://github.com/Z3Prover/z3', - license='MIT License', - keywords=['z3', 'smt', 'sat', 'prover', 'theorem'], - packages=['z3'], setup_requires = SETUP_REQUIRES, - install_requires = ["importlib-resources; python_version < '3.9'"], include_package_data=True, package_data={ 'z3': [os.path.join('lib', '*'), os.path.join('include', '*.h'), os.path.join('include', 'c++', '*.h')] diff --git a/src/api/python/test_dist_info.py b/src/api/python/test_dist_info.py new file mode 100755 index 000000000..13337419a --- /dev/null +++ b/src/api/python/test_dist_info.py @@ -0,0 +1,129 @@ +#!/usr/bin/env python3 +""" +Test script to validate that z3-solver creates dist-info when installed from source. +This test ensures that downstream packages can detect z3-solver properly. +""" + +import subprocess +import sys +import tempfile +import os +import shutil +from pathlib import Path + +def test_source_install_creates_dist_info(): + """Test that installing z3-solver from source creates dist-info directory.""" + print("Testing that source installation creates dist-info...") + + # Create a temporary virtual environment + with tempfile.TemporaryDirectory() as tmpdir: + venv_path = Path(tmpdir) / "test_venv" + + # Create virtual environment + result = subprocess.run([sys.executable, "-m", "venv", str(venv_path)], + capture_output=True, text=True) + if result.returncode != 0: + print(f"Failed to create venv: {result.stderr}") + return False + + # Determine the path to pip in the virtual environment + if sys.platform == "win32": + pip_path = venv_path / "Scripts" / "pip.exe" + python_path = venv_path / "Scripts" / "python.exe" + else: + pip_path = venv_path / "bin" / "pip" + python_path = venv_path / "bin" / "python" + + # Upgrade pip and setuptools + result = subprocess.run([str(pip_path), "install", "--upgrade", "pip", "setuptools"], + capture_output=True, text=True) + if result.returncode != 0: + print(f"Failed to upgrade pip/setuptools: {result.stderr}") + return False + + # Get the path to the z3 python package + z3_python_path = Path(__file__).parent.absolute() + + # Install z3-solver in editable mode without deps to avoid building C++ components + result = subprocess.run([str(pip_path), "install", "--no-deps", "--no-build-isolation", + "-e", str(z3_python_path)], + capture_output=True, text=True) + if result.returncode != 0: + print(f"Failed to install z3-solver: {result.stderr}") + return False + + # Check that dist-info directory was created + site_packages = venv_path / "lib" / f"python{sys.version_info.major}.{sys.version_info.minor}" / "site-packages" + if sys.platform == "win32": + site_packages = venv_path / "Lib" / "site-packages" + + dist_info_dirs = list(site_packages.glob("z3_solver*.dist-info")) + if not dist_info_dirs: + print(f"ERROR: No dist-info directory found in {site_packages}") + print("Available directories:") + for item in site_packages.iterdir(): + if item.is_dir(): + print(f" {item.name}") + return False + + dist_info_dir = dist_info_dirs[0] + print(f"SUCCESS: Found dist-info directory: {dist_info_dir.name}") + + # Check that the METADATA file exists and has proper content + metadata_file = dist_info_dir / "METADATA" + if not metadata_file.exists(): + print(f"ERROR: METADATA file not found in {dist_info_dir}") + return False + + metadata_content = metadata_file.read_text() + if "Name: z3-solver" not in metadata_content: + print(f"ERROR: METADATA file doesn't contain expected package name") + return False + + print("SUCCESS: METADATA file contains correct package information") + + # Test that the package can be detected by pip + result = subprocess.run([str(pip_path), "show", "z3-solver"], + capture_output=True, text=True) + if result.returncode != 0: + print(f"ERROR: pip show z3-solver failed: {result.stderr}") + return False + + if "Name: z3-solver" not in result.stdout: + print(f"ERROR: pip show output doesn't contain expected package name") + return False + + print("SUCCESS: pip can detect the installed package") + + # Test that Python can detect the package + python_test_script = ''' +import sys +try: + import importlib.metadata as metadata + dist = metadata.distribution("z3-solver") + print(f"Found package: {dist.name} {dist.version}") + sys.exit(0) +except metadata.PackageNotFoundError: + print("ERROR: Package not found by importlib.metadata") + sys.exit(1) +''' + + result = subprocess.run([str(python_path), "-c", python_test_script], + capture_output=True, text=True) + if result.returncode != 0: + print(f"ERROR: Python package detection failed: {result.stderr}") + return False + + print("SUCCESS: Python can detect the installed package") + print(f"Detection output: {result.stdout.strip()}") + + return True + +if __name__ == "__main__": + success = test_source_install_creates_dist_info() + if success: + print("\n✓ All tests passed! Source installation creates proper dist-info.") + sys.exit(0) + else: + print("\n✗ Test failed! Source installation does not create proper dist-info.") + sys.exit(1) \ No newline at end of file