diff --git a/sources b/sources index 3d592ee..5c660ed 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (z3-4.12.2.tar.gz) = 375477cbbc9837b44e752c89916409d07bf6a73830b52878aab4f376f08b37dd5ab485da225744d394ab15f2a7e1014edc3be5eb9962934c440a8d55259317e2 +SHA512 (z3-4.12.4.tar.gz) = fcb778d2e3e0d13fc68afcd8724548279f9edbbb4aac1bbb93e00959c33330ab2fd84f2c2e4b0b78f767819725a90b845fc606a9adc931ae1f0a11f4deae433b diff --git a/z3-escapes.patch b/z3-escapes.patch deleted file mode 100644 index 8d1e0c7..0000000 --- a/z3-escapes.patch +++ /dev/null @@ -1,205 +0,0 @@ -Fixes warnings such as these: - -/builddir/build/BUILD/z3-z3-4.12.2/scripts/mk_genfile_common.py:142: SyntaxWarning: invalid escape sequence '\-' - words = re.split('[^\-a-zA-Z0-9_]+', line) -/builddir/build/BUILD/z3-z3-4.12.2/scripts/mk_genfile_common.py:577: SyntaxWarning: invalid escape sequence '\W' - words = re.split('\W+', line) - ---- z3-z3-4.12.2/scripts/mk_genfile_common.py.orig 2023-05-12 13:59:04.000000000 -0600 -+++ z3-z3-4.12.2/scripts/mk_genfile_common.py 2023-07-06 10:52:08.477210179 -0600 -@@ -139,7 +139,7 @@ def mk_z3consts_py_internal(api_files, o - assert False, "Invalid %s, line: %s" % (api_file, linenum) - else: - assert mode == IN_ENUM -- words = re.split('[^\-a-zA-Z0-9_]+', line) -+ words = re.split('[^-a-zA-Z0-9_]+', line) - m = closebrace_pat.match(line) - if m: - name = words[1] -@@ -227,7 +227,7 @@ def mk_z3consts_dotnet_internal(api_file - assert False, "Invalid %s, line: %s" % (api_file, linenum) - else: - assert mode == IN_ENUM -- words = re.split('[^\-a-zA-Z0-9_]+', line) -+ words = re.split('[^-a-zA-Z0-9_]+', line) - m = closebrace_pat.match(line) - if m: - name = words[1] -@@ -315,7 +315,7 @@ def mk_z3consts_java_internal(api_files, - assert False, "Invalid %s, line: %s" % (api_file, linenum) - else: - assert mode == IN_ENUM -- words = re.split('[^\-a-zA-Z0-9_]+', line) -+ words = re.split('[^-a-zA-Z0-9_]+', line) - m = closebrace_pat.match(line) - if m: - name = words[1] -@@ -441,7 +441,7 @@ def mk_z3consts_ml_internal(api_files, o - assert False, "Invalid %s, line: %s" % (api_file, linenum) - else: - assert mode == IN_ENUM -- words = re.split('[^\-a-zA-Z0-9_]+', line) -+ words = re.split('[^-a-zA-Z0-9_]+', line) - m = closebrace_pat.match(line) - if m: - name = words[1] -@@ -574,7 +574,7 @@ def mk_def_file_internal(defname, dll_na - for line in api: - m = pat1.match(line) - if m: -- words = re.split('\W+', line) -+ words = re.split(r'\W+', line) - i = 0 - for w in words: - if w == 'Z3_API': -@@ -618,9 +618,9 @@ def mk_gparams_register_modules_internal - fout = open(fullname, 'w') - fout.write('// Automatically generated file.\n') - fout.write('#include "util/gparams.h"\n') -- reg_pat = re.compile('[ \t]*REG_PARAMS\(\'([^\']*)\'\)') -- reg_mod_pat = re.compile('[ \t]*REG_MODULE_PARAMS\(\'([^\']*)\', *\'([^\']*)\'\)') -- reg_mod_descr_pat = re.compile('[ \t]*REG_MODULE_DESCRIPTION\(\'([^\']*)\', *\'([^\']*)\'\)') -+ reg_pat = re.compile(r'[ \t]*REG_PARAMS\(\'([^\']*)\'\)') -+ reg_mod_pat = re.compile(r'[ \t]*REG_MODULE_PARAMS\(\'([^\']*)\', *\'([^\']*)\'\)') -+ reg_mod_descr_pat = re.compile(r'[ \t]*REG_MODULE_DESCRIPTION\(\'([^\']*)\', *\'([^\']*)\'\)') - for h_file in sorted_headers_by_component(h_files_full_path): - added_include = False - with io.open(h_file, encoding='utf-8', mode='r') as fin: -@@ -698,9 +698,9 @@ def mk_install_tactic_cpp_internal(h_fil - fout.write('#include "cmd_context/tactic_cmds.h"\n') - fout.write('#include "cmd_context/simplifier_cmds.h"\n') - fout.write('#include "cmd_context/cmd_context.h"\n') -- tactic_pat = re.compile('[ \t]*ADD_TACTIC\(.*\)') -- probe_pat = re.compile('[ \t]*ADD_PROBE\(.*\)') -- simplifier_pat = re.compile('[ \t]*ADD_SIMPLIFIER\(.*\)') -+ tactic_pat = re.compile(r'[ \t]*ADD_TACTIC\(.*\)') -+ probe_pat = re.compile(r'[ \t]*ADD_PROBE\(.*\)') -+ simplifier_pat = re.compile(r'[ \t]*ADD_SIMPLIFIER\(.*\)') - for h_file in sorted_headers_by_component(h_files_full_path): - added_include = False - try: -@@ -780,10 +780,10 @@ def mk_mem_initializer_cpp_internal(h_fi - fullname = os.path.join(path, 'mem_initializer.cpp') - fout = open(fullname, 'w') - fout.write('// Automatically generated file.\n') -- initializer_pat = re.compile('[ \t]*ADD_INITIALIZER\(\'([^\']*)\'\)') -+ initializer_pat = re.compile(r'[ \t]*ADD_INITIALIZER\(\'([^\']*)\'\)') - # ADD_INITIALIZER with priority -- initializer_prio_pat = re.compile('[ \t]*ADD_INITIALIZER\(\'([^\']*)\',[ \t]*(-?[0-9]*)\)') -- finalizer_pat = re.compile('[ \t]*ADD_FINALIZER\(\'([^\']*)\'\)') -+ initializer_prio_pat = re.compile(r'[ \t]*ADD_INITIALIZER\(\'([^\']*)\',[ \t]*(-?[0-9]*)\)') -+ finalizer_pat = re.compile(r'[ \t]*ADD_FINALIZER\(\'([^\']*)\'\)') - for h_file in sorted_headers_by_component(h_files_full_path): - added_include = False - with io.open(h_file, encoding='utf-8', mode='r') as fin: ---- z3-z3-4.12.2/scripts/mk_util.py.orig 2023-07-06 11:53:06.045350565 -0600 -+++ z3-z3-4.12.2/scripts/mk_util.py 2023-07-06 12:02:59.686951602 -0600 -@@ -395,7 +395,7 @@ def check_java(): - else: - # Search for jni.h in the library directories... - t = open('errout', 'r') -- open_pat = re.compile("\[search path for class files: (.*)\]") -+ open_pat = re.compile(r"\[search path for class files: (.*)\]") - cdirs = [] - for line in t: - m = open_pat.match(line) -@@ -808,8 +808,8 @@ def parse_options(): - def extract_c_includes(fname): - result = {} - # We look for well behaved #include directives -- std_inc_pat = re.compile("[ \t]*#include[ \t]*\"(.*)\"[ \t]*") -- system_inc_pat = re.compile("[ \t]*#include[ \t]*\<.*\>[ \t]*") -+ std_inc_pat = re.compile(r"[ \t]*#include[ \t]*\"(.*)\"[ \t]*") -+ system_inc_pat = re.compile(r"[ \t]*#include[ \t]*\<.*\>[ \t]*") - # We should generate and error for any occurrence of #include that does not match the previous pattern. - non_std_inc_pat = re.compile(".*#include.*") - -@@ -1716,7 +1716,7 @@ class DotNetDLLComponent(Component): - - print("Version output to csproj:", version) - -- core_csproj_str = """ -+ core_csproj_str = r""" - - - netstandard1.4 -@@ -2237,7 +2237,7 @@ class DotNetExampleComponent(ExampleComp - else: - platform = 'x86' - -- dotnet_proj_str = """ -+ dotnet_proj_str = r""" - - Exe - netcoreapp2.0 -@@ -3153,7 +3153,7 @@ def mk_vs_proj_property_groups(f, name, - f.write(' Win32Proj\n') - f.write(' %s\n' % get_platform_toolset_str()) - f.write(' \n') -- f.write(' \n') -+ f.write(' \n') - f.write(' \n') - f.write(' %s\n' % type) - f.write(' Unicode\n') -@@ -3164,24 +3164,24 @@ def mk_vs_proj_property_groups(f, name, - f.write(' Unicode\n') - f.write(' false\n') - f.write(' \n') -- f.write(' \n') -+ f.write(' \n') - f.write(' \n') - f.write(' \n') -- f.write(' \n') -+ f.write(' \n') - f.write(' \n') - f.write(' \n') -- f.write(' $(SolutionDir)\$(ProjectName)\$(Configuration)\\n') -+ f.write(' $(SolutionDir)\\$(ProjectName)\\$(Configuration)\\\n') - f.write(' %s\n' % name) - f.write(' .%s\n' % target_ext) -- f.write(' $(SolutionDir)\$(ProjectName)\$(Configuration)\\n') -+ f.write(' $(SolutionDir)\\$(ProjectName)\\$(Configuration)\\\n') - f.write(' %s\n' % name) - f.write(' .%s\n' % target_ext) - f.write(' \n') - f.write(' \n') -- f.write(' $(ProjectName)\$(Configuration)\\n') -+ f.write(' $(ProjectName)\\$(Configuration)\\\n') - f.write(' \n') - f.write(' \n') -- f.write(' $(ProjectName)\$(Configuration)\\n') -+ f.write(' $(ProjectName)\\$(Configuration)\\\n') - f.write(' \n') - - -@@ -3258,7 +3258,7 @@ def mk_vs_proj(name, components): - mk_vs_proj_link_exe(f, name, debug=False) - f.write(' \n') - mk_vs_proj_dep_groups(f, name, components) -- f.write(' \n') -+ f.write(' \n') - f.write(' \n') - f.write(' \n') - f.write('\n') -@@ -3299,7 +3299,7 @@ def mk_vs_proj_dll(name, components): - mk_vs_proj_link_dll(f, name, debug=False) - f.write(' \n') - mk_vs_proj_dep_groups(f, name, components) -- f.write(' \n') -+ f.write(' \n') - f.write(' \n') - f.write(' \n') - f.write('\n') ---- z3-z3-4.12.2/scripts/update_api.py.orig 2023-07-06 12:02:07.510504547 -0600 -+++ z3-z3-4.12.2/scripts/update_api.py 2023-07-06 12:02:19.399378554 -0600 -@@ -116,8 +116,8 @@ class APITypes: - - def def_Types(self, api_files): - global Closures -- pat1 = re.compile(" *def_Type\(\'(.*)\',[^\']*\'(.*)\',[^\']*\'(.*)\'\)[ \t]*") -- pat2 = re.compile("Z3_DECLARE_CLOSURE\((.*),(.*), \((.*)\)\)") -+ pat1 = re.compile(r" *def_Type\(\'(.*)\',[^\']*\'(.*)\',[^\']*\'(.*)\'\)[ \t]*") -+ pat2 = re.compile(r"Z3_DECLARE_CLOSURE\((.*),(.*), \((.*)\)\)") - for api_file in api_files: - with open(api_file, 'r') as api: - for line in api: diff --git a/z3-python.patch b/z3-python.patch deleted file mode 100644 index c26dd68..0000000 --- a/z3-python.patch +++ /dev/null @@ -1,21 +0,0 @@ ---- a/scripts/update_api.py 2020-09-10 12:51:28.000000000 -0600 -+++ b/scripts/update_api.py 2020-12-25 17:03:00.196777823 -0700 -@@ -1755,15 +1755,15 @@ def write_core_py_preamble(core_py): - # Automatically generated file - import sys, os - import ctypes --import pkg_resources -+import sysconfig - from .z3types import * - from .z3consts import * - --_ext = 'dll' if sys.platform in ('win32', 'cygwin') else 'dylib' if sys.platform == 'darwin' else 'so' -+_ext = 'dll' if sys.platform in ('win32', 'cygwin') else 'dylib' if sys.platform == 'darwin' else 'so.@MAJVER@' - _lib = None - _default_dirs = ['.', - os.path.dirname(os.path.abspath(__file__)), -- pkg_resources.resource_filename('z3', 'lib'), -+ sysconfig.get_config_var('LIBDIR'), - os.path.join(sys.prefix, 'lib'), - None] - _all_dirs = [] diff --git a/z3-stdint.patch b/z3-stdint.patch deleted file mode 100644 index c0874f2..0000000 --- a/z3-stdint.patch +++ /dev/null @@ -1,25 +0,0 @@ -Fixes errors such as these: - -In file included from /builddir/build/BUILD/z3-z3-4.12.2/src/util/region.cpp:53: -/builddir/build/BUILD/z3-z3-4.12.2/src/util/region.cpp: In member function ‘void* region::allocate(size_t)’: -/builddir/build/BUILD/z3-z3-4.12.2/src/util/tptr.h:29:62: error: ‘uintptr_t’ does not name a type - 29 | #define ALIGN(T, PTR) reinterpret_cast(((reinterpret_cast(PTR) >> PTR_ALIGNMENT) + \ - | ^~~~~~~~~ -/builddir/build/BUILD/z3-z3-4.12.2/src/util/region.cpp:82:22: note: in expansion of macro ‘ALIGN’ - 82 | m_curr_ptr = ALIGN(char *, new_curr_ptr); - | ^~~~~ -/builddir/build/BUILD/z3-z3-4.12.2/src/util/region.cpp:57:1: note: ‘uintptr_t’ is defined in header ‘’; did you forget to ‘#include ’? - 56 | #include "util/page.h" - +++ |+#include - 57 | - ---- z3-z3-4.12.2/src/util/tptr.h.orig 2023-05-12 13:59:04.000000000 -0600 -+++ z3-z3-4.12.2/src/util/tptr.h 2023-05-13 07:04:48.389716628 -0600 -@@ -19,6 +19,7 @@ Revision History: - - #pragma once - -+#include - #include "util/machine.h" - - #define TAG_SHIFT PTR_ALIGNMENT diff --git a/z3.spec b/z3.spec index 501ce62..1c1163b 100644 --- a/z3.spec +++ b/z3.spec @@ -12,8 +12,8 @@ %bcond_with test Name: z3 -Version: 4.12.2 -Release: 7%{?dist} +Version: 4.12.4 +Release: 1%{?dist} Summary: Satisfiability Modulo Theories (SMT) solver License: MIT @@ -21,14 +21,6 @@ URL: https://github.com/Z3Prover/z3 Source0: https://github.com/Z3Prover/z3/archive/%{name}-%{version}.tar.gz # Do not try to build or install native OCaml artifacts on bytecode-only arches Patch0: %{name}-ocaml.patch -# Change the way python finds the shared object; see bz 1910923 -Patch1: %{name}-python.patch -# Add a missing include of cstdint -# https://github.com/Z3Prover/z3/pull/6720 -Patch2: %{name}-stdint.patch -# Fix malformed python escape sequences -# https://github.com/Z3Prover/z3/pull/6797 -Patch3: %{name}-escapes.patch BuildRequires: cmake BuildRequires: doxygen @@ -317,6 +309,10 @@ cd - %{python3_sitelib}/z3/ %changelog +* Sat Dec 9 2023 Jerry James - 4.12.4-1 +- Version 4.12.4 +- Drop upstreamed patches: python, stdint, escapes + * Thu Oct 05 2023 Richard W.M. Jones - 4.12.2-7 - OCaml 5.1 rebuild for Fedora 40