mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-18 02:16:40 +00:00
Code Activity

Revert "Revert "Fix source installation to create dist-info directory for pac…"

Browse source 
This reverts commit 661ccb3702.
This commit is contained in:
Nikolaj Bjorner 2025-06-29 09:12:38 -07:00 • committed by GitHub
parent 661ccb3702
commit bf771eb5a4
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
4 changed files with 329 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

140
src/api/python/demonstrate_fix.py Executable file
View file

@ -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)

51
src/api/python/pyproject.toml
View file

@ -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/*"]

22
src/api/python/setup.py
View file

@ -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')]

129
src/api/python/test_dist_info.py Executable file
View file

@ -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)