Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add z3 fix by removing the requirement for python3-distutils. #25890

Merged
merged 1 commit into from
May 22, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
100 changes: 100 additions & 0 deletions packages/z3/z3.4.13.0-1/files/libatomic.patch
Original file line number Diff line number Diff line change
@@ -0,0 +1,100 @@
diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 014b0e40f..3e6da0b22 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -314,6 +314,26 @@ def test_fpmath(cc):
FPMATH_FLAGS=""
return "UNKNOWN"

+def test_atomic_required(cc):
+ t = TempFile('tstatomic.cpp')
+ t.add("""
+ #include <atomic>
+ std::atomic<int> x;
+ std::atomic<short> y;
+ std::atomic<char> z;
+ std::atomic<long long> w;
+ int main() {
+ ++z;
+ ++y;
+ ++w;
+ return ++x;
+ }
+ """)
+ t.commit()
+ fails_without = exec_compiler_cmd([cc, CPPFLAGS, '', 'tstatomic.cpp', LDFLAGS, '']) != 0
+ ok_with = exec_compiler_cmd([cc, CPPFLAGS, '', 'tstatomic.cpp', LDFLAGS + ' -latomic', '']) == 0
+ return fails_without and ok_with
+

def find_jni_h(path):
for root, dirs, files in os.walk(path):
@@ -555,19 +575,19 @@ def set_version(major, minor, build, revision):
print("Set Assembly Version (BUILD):", VER_MAJOR, VER_MINOR, VER_BUILD, VER_TWEAK)
return

- # use parameters to set up version if not provided by script args
+ # use parameters to set up version if not provided by script args
VER_MAJOR = major
VER_MINOR = minor
VER_BUILD = build
VER_TWEAK = revision

- # update VER_TWEAK base on github
+ # update VER_TWEAK base on github
if GIT_DESCRIBE:
branch = check_output(['git', 'rev-parse', '--abbrev-ref', 'HEAD'])
VER_TWEAK = int(check_output(['git', 'rev-list', '--count', 'HEAD']))
-
+
print("Set Assembly Version (DEFAULT):", VER_MAJOR, VER_MINOR, VER_BUILD, VER_TWEAK)
-
+
def get_version():
return (VER_MAJOR, VER_MINOR, VER_BUILD, VER_TWEAK)

@@ -1858,7 +1878,7 @@ class JavaDLLComponent(Component):
os.path.join('api', 'java', 'Native'))
elif IS_OSX and IS_ARCH_ARM64:
out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) -arch arm64 %s$(OBJ_EXT) libz3$(SO_EXT)\n' %
- os.path.join('api', 'java', 'Native'))
+ os.path.join('api', 'java', 'Native'))
else:
out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) %s$(OBJ_EXT) libz3$(SO_EXT)\n' %
os.path.join('api', 'java', 'Native'))
@@ -2600,6 +2620,9 @@ def mk_config():
CXXFLAGS = '%s -fvisibility=hidden -fvisibility-inlines-hidden -c' % CXXFLAGS
FPMATH = test_fpmath(CXX)
CXXFLAGS = '%s %s' % (CXXFLAGS, FPMATH_FLAGS)
+ atomic_required = test_atomic_required(CXX)
+ if atomic_required:
+ LDFLAGS = '%s -latomic' % LDFLAGS
if LOG_SYNC:
CXXFLAGS = '%s -DZ3_LOG_SYNC' % CXXFLAGS
if SINGLE_THREADED:
@@ -2710,6 +2733,7 @@ def mk_config():
print('Prefix: %s' % PREFIX)
print('64-bit: %s' % is64())
print('FP math: %s' % FPMATH)
+ print('libatomic: %s' % ('required' if atomic_required else 'not required'))
print("Python pkg dir: %s" % PYTHON_PACKAGE_DIR)
if GPROF:
print('gprof: enabled')
@@ -2854,7 +2878,7 @@ def update_version():
revision = VER_TWEAK

print("UpdateVersion:", get_full_version_string(major, minor, build, revision))
-
+
if major is None or minor is None or build is None or revision is None:
raise MKException("set_version(major, minor, build, revision) must be used before invoking update_version()")
if not ONLY_MAKEFILES:
@@ -3068,7 +3092,7 @@ def mk_bindings(api_files):
z3py_output_dir=get_z3py_dir(),
dotnet_output_dir=dotnet_output_dir,
java_input_dir=java_input_dir,
- java_output_dir=java_output_dir,
+ java_output_dir=java_output_dir,
java_package_name=java_package_name,
ml_output_dir=ml_output_dir,
ml_src_dir=ml_output_dir
43 changes: 43 additions & 0 deletions packages/z3/z3.4.13.0-1/opam
Original file line number Diff line number Diff line change
@@ -0,0 +1,43 @@
opam-version: "2.0"
maintainer: "weng@cs.jhu.edu"
authors: "MSR"
homepage: "https://github.com/Z3prover/z3"
bug-reports: "https://github.com/Z3prover/z3/issues"
license: "MIT"
dev-repo: "git+https://github.com/Z3prover/z3.git"
patches: [
"libatomic.patch"
]
build: [
[ "python3" "scripts/mk_make.py" "--ml" ]
[ make "-C" "build" "-j" jobs ]
]

install: [
[ "sh" "-c" "ocamlfind install z3 build/api/ml/* -dll build/libz3.*"]
[ "cp" "build/z3" "%{bin}%/z3"]
]

depends: [
"ocaml" {>= "4.08.0"}
"ocamlfind" {build}
"zarith"
"conf-gmp"
"conf-python-3" {build}
"conf-c++" {build}
]
x-ci-accept-failures: [
"centos-7" "oraclelinux-7" # C compiler is too old
]
conflicts: [
"ocaml-option-bytecode-only"
]
synopsis: "Z3 solver"
url {
src:
"https://github.com/Z3Prover/z3/archive/refs/tags/z3-4.13.0.tar.gz"
checksum: [
"sha256=01bcc61c8362e37bb89fd2430f7e3385e86df7915019bd2ce45de9d9bd934502"
"sha512=8503787fe0b18592b5a131bcec2cacfa5f5096d76386a1c4fda7a836e472924b154433306d27600ff0d0758ddb710c965901fbfc2e5605919b624b9d4d1bc4fd"
]
}