diff --git a/src/api/python/demonstrate_fix.py b/src/api/python/demonstrate_fix.py deleted file mode 100755 index bc2ca19bf..000000000 --- a/src/api/python/demonstrate_fix.py +++ /dev/null @@ -1,140 +0,0 @@ -#!/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 54c401c28..380744c87 100644 --- a/src/api/python/pyproject.toml +++ b/src/api/python/pyproject.toml @@ -1,54 +1,3 @@ [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 c6fdf7205..4d26367b3 100644 --- a/src/api/python/setup.py +++ b/src/api/python/setup.py @@ -9,11 +9,7 @@ import glob from setuptools import setup from setuptools.command.build import build as _build from setuptools.command.sdist import sdist as _sdist -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.bdist_wheel import bdist_wheel as _bdist_wheel from setuptools.command.develop import develop as _develop class LibError(Exception): @@ -116,7 +112,6 @@ 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') @@ -289,7 +284,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(r"(.+)\_7") +internal_build_re = re.compile("(.+)\_7") class bdist_wheel(_bdist_wheel): @@ -328,10 +323,19 @@ class bdist_wheel(_bdist_wheel): setup( - # Most configuration is now in pyproject.toml - # Keep only setup.py-specific configuration + 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', + 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 deleted file mode 100755 index 13337419a..000000000 --- a/src/api/python/test_dist_info.py +++ /dev/null @@ -1,129 +0,0 @@ -#!/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