-
Notifications
You must be signed in to change notification settings - Fork 1.1k
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Add z3 fix by removing the requirement for
python3-distutils
.
- Loading branch information
Showing
2 changed files
with
143 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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" | ||
] | ||
} |