From b4c9000b463a090b40ccb4112e2928fe1bb24141 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Mon, 10 Jul 2023 16:55:13 -0600 Subject: [PATCH] OCaml 5.0.0 rebuild --- z3-escapes.patch | 205 +++++++++++++++++++++++++++++++++++++++++++++++ z3-ocaml.patch | 56 +++++++++++++ z3.spec | 32 ++++++-- 3 files changed, 285 insertions(+), 8 deletions(-) create mode 100644 z3-escapes.patch create mode 100644 z3-ocaml.patch diff --git a/z3-escapes.patch b/z3-escapes.patch new file mode 100644 index 0000000..8d1e0c7 --- /dev/null +++ b/z3-escapes.patch @@ -0,0 +1,205 @@ +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-ocaml.patch b/z3-ocaml.patch new file mode 100644 index 0000000..32e0857 --- /dev/null +++ b/z3-ocaml.patch @@ -0,0 +1,56 @@ +--- z3-z3-4.12.2/scripts/mk_util.py.orig 2023-05-12 13:59:04.000000000 -0600 ++++ z3-z3-4.12.2/scripts/mk_util.py 2023-07-06 11:53:06.045350565 -0600 +@@ -34,7 +34,7 @@ EXAMP_DEBUG_FLAG='' + LDFLAGS=getenv("LDFLAGS", "") + JNI_HOME=getenv("JNI_HOME", None) + OCAMLC=getenv("OCAMLC", "ocamlc") +-OCAMLOPT=getenv("OCAMLOPT", "ocamlopt") ++OCAMLOPT=getenv("OCAMLOPT", None) + OCAML_LIB=getenv("OCAML_LIB", None) + OCAMLFIND=getenv("OCAMLFIND", "ocamlfind") + DOTNET="dotnet" +@@ -460,13 +460,9 @@ def check_ml(): + raise MKException('Failed testing ocamlc compiler. Set environment variable OCAMLC with the path to the Ocaml compiler') + if is_verbose(): + print ('Testing %s...' % OCAMLOPT) +- r = exec_cmd([OCAMLOPT, '-o', 'a.out', 'hello.ml']) +- if r != 0: +- raise MKException('Failed testing ocamlopt compiler. Set environment variable OCAMLOPT with the path to the Ocaml native compiler. Note that ocamlopt may require flexlink to be in your path.') + try: + rmf('hello.cmi') + rmf('hello.cmo') +- rmf('hello.cmx') + rmf('a.out') + rmf('hello.o') + except: +@@ -2069,7 +2065,7 @@ class MLComponent(Component): + out.write('\t%s -linkall -shared -o %s.cmxs -I . -I %s %s.cmxa\n' % (OCAMLOPTF, z3mls, self.sub_dir, z3mls)) + + out.write('\n') +- out.write('ml: %s.cma %s.cmxa %s.cmxs\n' % (z3mls, z3mls, z3mls)) ++ out.write('ml: %s.cma\n' % z3mls) + if IS_OSX: + out.write('\tinstall_name_tool -id %s/libz3.dylib libz3.dylib\n' % (stubs_install_path)) + out.write('\tinstall_name_tool -change libz3.dylib %s/libz3.dylib api/ml/dllz3ml.so\n' % (stubs_install_path)) +@@ -2091,8 +2087,6 @@ class MLComponent(Component): + out.write(get_component(Z3_DLL_COMPONENT).dll_name + '$(SO_EXT) ') + out.write(os.path.join(self.sub_dir, 'META ')) + out.write(os.path.join(self.sub_dir, 'z3ml.cma ')) +- out.write(os.path.join(self.sub_dir, 'z3ml.cmxa ')) +- out.write(os.path.join(self.sub_dir, 'z3ml.cmxs ')) + + def mk_install(self, out): + if is_ml_enabled() and self._install_bindings(): +@@ -2119,12 +2113,9 @@ class MLComponent(Component): + else: + out.write(' ' + os.path.join(self.sub_dir, m) + '.mli') + out.write(' ' + os.path.join(self.sub_dir, m) + '.cmi') +- out.write(' ' + os.path.join(self.sub_dir, m) + '.cmx') + out.write(' %s' % ((os.path.join(self.sub_dir, 'libz3ml$(LIB_EXT)')))) + out.write(' %s' % ((os.path.join(self.sub_dir, 'z3ml$(LIB_EXT)')))) + out.write(' %s' % ((os.path.join(self.sub_dir, 'z3ml.cma')))) +- out.write(' %s' % ((os.path.join(self.sub_dir, 'z3ml.cmxa')))) +- out.write(' %s' % ((os.path.join(self.sub_dir, 'z3ml.cmxs')))) + out.write(' %s' % ((os.path.join(self.sub_dir, 'dllz3ml')))) + if is_windows() or is_cygwin_mingw() or is_msys2(): + out.write('.dll') diff --git a/z3.spec b/z3.spec index ca3ac91..78e4b3e 100644 --- a/z3.spec +++ b/z3.spec @@ -19,11 +19,16 @@ Summary: Satisfiability Modulo Theories (SMT) solver License: MIT 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 -Patch0: %{name}-python.patch +Patch1: %{name}-python.patch # Add a missing include of cstdint # https://github.com/Z3Prover/z3/pull/6720 -Patch1: %{name}-stdint.patch +Patch2: %{name}-stdint.patch +# Fix malformed python escape sequences +# https://github.com/Z3Prover/z3/pull/6797 +Patch3: %{name}-escapes.patch BuildRequires: cmake BuildRequires: doxygen @@ -146,7 +151,11 @@ Requires: z3-libs = %{version}-%{release} Python 3 interface to z3. %prep -%autosetup -p1 -n %{name}-%{name}-%{version} +%autosetup -N -n %{name}-%{name}-%{version} +%ifnarch %{ocaml_native_compiler} +%patch -P0 -p1 +%endif +%autopatch -m 1 -p1 # Enable verbose builds, use Fedora CFLAGS, preserve timestamps when installing, # include the entire contents of the archives in the library, link the library @@ -221,12 +230,15 @@ mv %{buildroot}%{_libdir}/libz3java.so %{buildroot}%{_libdir}/z3 %endif # Install the OCaml interface -pushd build/api/ml +cd build/api/ml mkdir -p %{buildroot}%{ocamldir}/Z3 -cp -p META *.{a,cma,cmi,cmx,cmxa,cmxs,mli} %{buildroot}%{ocamldir}/Z3 +%ifarch %{ocaml_native_compiler} +cp -p *.cmx{,a,s} %{buildroot}%{ocamldir}/Z3 +%endif +cp -p META *.{a,cma,cmi,mli} %{buildroot}%{ocamldir}/Z3 mkdir -p %{buildroot}%{ocamldir}/stublibs cp -p *.so %{buildroot}%{ocamldir}/stublibs -popd +cd - # We handle the documentation files below rm -rf %{buildroot}%{_docdir}/Z3 @@ -277,21 +289,25 @@ cd - %{ocamldir}/Z3/META %{ocamldir}/Z3/*.cma %{ocamldir}/Z3/*.cmi +%ifarch %{ocaml_native_compiler} %{ocamldir}/Z3/*.cmxs +%endif %{ocamldir}/stublibs/*.so %files -n ocaml-z3-devel %{ocamldir}/Z3/*.a +%ifarch %{ocaml_native_compiler} %{ocamldir}/Z3/*.cmx %{ocamldir}/Z3/*.cmxa +%endif %{ocamldir}/Z3/*.mli %files -n python3-z3 %{python3_sitelib}/z3/ %changelog -* Wed Jun 21 2023 Jerry James - 4.12.2-3 -- Rebuild for OCaml 5.0 +* Mon Jul 10 2023 Jerry James - 4.12.2-3 +- OCaml 5.0.0 rebuild * Thu Jun 15 2023 Python Maint - 4.12.2-2 - Rebuilt for Python 3.12