mirror of
https://github.com/Z3Prover/z3
synced 2025-08-12 06:00:53 +00:00
Add proper pyproject.toml metadata for dist-info creation
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot]
parent
dbefbfb89f
commit
7f5be8814b
4 changed files with 240 additions and 16 deletions
|
|
@ -1,3 +1,52 @@
|
|||
[build-system]
|
||||
requires = ["setuptools>=70"]
|
||||
build-backend = "setuptools.build_meta"
|
||||
|
||||
[project]
|
||||
name = "z3-solver"
|
||||
description = "an efficient SMT solver library"
|
||||
readme = "README.txt"
|
||||
requires-python = ">=3.8"
|
||||
license = "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'"
|
||||
]
|
||||
dynamic = ["version"]
|
||||
|
||||
[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.dynamic]
|
||||
version = {attr = "z3_version.__version__"}
|
||||
|
|
|
|||
|
|
@ -112,21 +112,27 @@ def _clean_native_build():
|
|||
rmtree(BUILD_DIR)
|
||||
|
||||
def _z3_version():
|
||||
post = os.getenv('Z3_VERSION_SUFFIX', '')
|
||||
if RELEASE_DIR is None:
|
||||
fn = os.path.join(SRC_DIR, 'scripts', 'mk_project.py')
|
||||
if os.path.exists(fn):
|
||||
with open(fn) as f:
|
||||
for line in f:
|
||||
n = re.match(r".*set_version\((.*), (.*), (.*), (.*)\).*", line)
|
||||
if not n is None:
|
||||
return n.group(1) + '.' + n.group(2) + '.' + n.group(3) + '.' + n.group(4) + post
|
||||
return "?.?.?.?"
|
||||
else:
|
||||
version = RELEASE_METADATA[0]
|
||||
if version.count('.') == 2:
|
||||
version += '.0'
|
||||
return version + post
|
||||
# Import version from z3_version module for consistency
|
||||
try:
|
||||
from z3_version import get_version
|
||||
return get_version()
|
||||
except ImportError:
|
||||
# Fallback to original implementation
|
||||
post = os.getenv('Z3_VERSION_SUFFIX', '')
|
||||
if RELEASE_DIR is None:
|
||||
fn = os.path.join(SRC_DIR, 'scripts', 'mk_project.py')
|
||||
if os.path.exists(fn):
|
||||
with open(fn) as f:
|
||||
for line in f:
|
||||
n = re.match(r".*set_version\((.*), (.*), (.*), (.*)\).*", line)
|
||||
if not n is None:
|
||||
return n.group(1) + '.' + n.group(2) + '.' + n.group(3) + '.' + n.group(4) + post
|
||||
return "?.?.?.?"
|
||||
else:
|
||||
version = RELEASE_METADATA[0]
|
||||
if version.count('.') == 2:
|
||||
version += '.0'
|
||||
return version + post
|
||||
|
||||
def _configure_z3():
|
||||
global IS_SINGLE_THREADED
|
||||
|
|
@ -284,7 +290,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):
|
||||
|
||||
|
|
|
|||
129
src/api/python/test_dist_info.py
Executable file
129
src/api/python/test_dist_info.py
Executable 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)
|
||||
40
src/api/python/z3_version.py
Normal file
40
src/api/python/z3_version.py
Normal file
|
|
@ -0,0 +1,40 @@
|
|||
"""
|
||||
Version detection for z3-solver package.
|
||||
"""
|
||||
import os
|
||||
import re
|
||||
|
||||
def get_version():
|
||||
"""Get the z3 version from the source tree."""
|
||||
post = os.getenv('Z3_VERSION_SUFFIX', '')
|
||||
|
||||
# Determine where the source directory is located
|
||||
ROOT_DIR = os.path.abspath(os.path.dirname(__file__))
|
||||
SRC_DIR_LOCAL = os.path.join(ROOT_DIR, 'core')
|
||||
SRC_DIR_REPO = os.path.join(ROOT_DIR, '..', '..', '..')
|
||||
SRC_DIR = SRC_DIR_LOCAL if os.path.exists(SRC_DIR_LOCAL) else SRC_DIR_REPO
|
||||
|
||||
# Check if we're using a release directory
|
||||
RELEASE_DIR = os.environ.get('PACKAGE_FROM_RELEASE', None)
|
||||
|
||||
if RELEASE_DIR is None:
|
||||
fn = os.path.join(SRC_DIR, 'scripts', 'mk_project.py')
|
||||
if os.path.exists(fn):
|
||||
with open(fn) as f:
|
||||
for line in f:
|
||||
n = re.match(r".*set_version\((.*), (.*), (.*), (.*)\).*", line)
|
||||
if not n is None:
|
||||
return n.group(1) + '.' + n.group(2) + '.' + n.group(3) + '.' + n.group(4) + post
|
||||
return "4.15.3.0" + post # fallback version
|
||||
else:
|
||||
RELEASE_METADATA = os.path.basename(RELEASE_DIR).split('-')
|
||||
if RELEASE_METADATA[0] == 'z3' and len(RELEASE_METADATA) >= 4:
|
||||
RELEASE_METADATA.pop(0)
|
||||
version = RELEASE_METADATA[0]
|
||||
if version.count('.') == 2:
|
||||
version += '.0'
|
||||
return version + post
|
||||
return "4.15.3.0" + post # fallback version
|
||||
|
||||
# Make version available at module level
|
||||
__version__ = get_version()
|
||||
Loading…
Add table
Add a link
Reference in a new issue