Compare commits
12 Commits
0c0af7bf22
...
6e97219e4f
Author | SHA1 | Date | |
---|---|---|---|
|
6e97219e4f | ||
|
75819831d1 | ||
|
e32772559e | ||
|
7ce32a5a19 | ||
|
8f4eee1504 | ||
|
7fe18e3f96 | ||
|
332c05596a | ||
|
a9a7082547 | ||
|
b4c9000b46 | ||
|
67bb880db8 | ||
|
647df7bf04 | ||
|
ee66c97a95 |
2
sources
2
sources
@ -1 +1 @@
|
|||||||
SHA512 (z3-4.12.1.tar.gz) = 031fba9cc000a8da0025f95fa3f1c7519071d1b7775b377ff3192c505bb4c7e3d267da246c9ae68c940224e055a3c30571d2c0d7fbb042ec9a3d5849543a385c
|
SHA512 (z3-4.12.2.tar.gz) = 375477cbbc9837b44e752c89916409d07bf6a73830b52878aab4f376f08b37dd5ab485da225744d394ab15f2a7e1014edc3be5eb9962934c440a8d55259317e2
|
||||||
|
205
z3-escapes.patch
Normal file
205
z3-escapes.patch
Normal file
@ -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 = """<Project Sdk="Microsoft.NET.Sdk">
|
||||||
|
+ core_csproj_str = r"""<Project Sdk="Microsoft.NET.Sdk">
|
||||||
|
|
||||||
|
<PropertyGroup>
|
||||||
|
<TargetFramework>netstandard1.4</TargetFramework>
|
||||||
|
@@ -2237,7 +2237,7 @@ class DotNetExampleComponent(ExampleComp
|
||||||
|
else:
|
||||||
|
platform = 'x86'
|
||||||
|
|
||||||
|
- dotnet_proj_str = """<Project Sdk="Microsoft.NET.Sdk">
|
||||||
|
+ dotnet_proj_str = r"""<Project Sdk="Microsoft.NET.Sdk">
|
||||||
|
<PropertyGroup>
|
||||||
|
<OutputType>Exe</OutputType>
|
||||||
|
<TargetFramework>netcoreapp2.0</TargetFramework>
|
||||||
|
@@ -3153,7 +3153,7 @@ def mk_vs_proj_property_groups(f, name,
|
||||||
|
f.write(' <Keyword>Win32Proj</Keyword>\n')
|
||||||
|
f.write(' <PlatformToolset>%s</PlatformToolset>\n' % get_platform_toolset_str())
|
||||||
|
f.write(' </PropertyGroup>\n')
|
||||||
|
- f.write(' <Import Project="$(VCTargetsPath)\Microsoft.Cpp.Default.props" />\n')
|
||||||
|
+ f.write(' <Import Project="$(VCTargetsPath)\\Microsoft.Cpp.Default.props" />\n')
|
||||||
|
f.write(' <PropertyGroup Condition="\'$(Configuration)|$(Platform)\'==\'Debug|Win32\'" Label="Configuration">\n')
|
||||||
|
f.write(' <ConfigurationType>%s</ConfigurationType>\n' % type)
|
||||||
|
f.write(' <CharacterSet>Unicode</CharacterSet>\n')
|
||||||
|
@@ -3164,24 +3164,24 @@ def mk_vs_proj_property_groups(f, name,
|
||||||
|
f.write(' <CharacterSet>Unicode</CharacterSet>\n')
|
||||||
|
f.write(' <UseOfMfc>false</UseOfMfc>\n')
|
||||||
|
f.write(' </PropertyGroup>\n')
|
||||||
|
- f.write(' <Import Project="$(VCTargetsPath)\Microsoft.Cpp.props" />\n')
|
||||||
|
+ f.write(' <Import Project="$(VCTargetsPath)\\Microsoft.Cpp.props" />\n')
|
||||||
|
f.write(' <ImportGroup Label="ExtensionSettings" />\n')
|
||||||
|
f.write(' <ImportGroup Label="PropertySheets">\n')
|
||||||
|
- f.write(' <Import Project="$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props" Condition="exists(\'$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props\')" Label="LocalAppDataPlatform" /> </ImportGroup>\n')
|
||||||
|
+ f.write(' <Import Project="$(UserRootDir)\\Microsoft.Cpp.$(Platform).user.props" Condition="exists(\'$(UserRootDir)\\Microsoft.Cpp.$(Platform).user.props\')" Label="LocalAppDataPlatform" /> </ImportGroup>\n')
|
||||||
|
f.write(' <PropertyGroup Label="UserMacros" />\n')
|
||||||
|
f.write(' <PropertyGroup>\n')
|
||||||
|
- f.write(' <OutDir Condition="\'$(Configuration)|$(Platform)\'==\'Debug|Win32\'">$(SolutionDir)\$(ProjectName)\$(Configuration)\</OutDir>\n')
|
||||||
|
+ f.write(' <OutDir Condition="\'$(Configuration)|$(Platform)\'==\'Debug|Win32\'">$(SolutionDir)\\$(ProjectName)\\$(Configuration)\\</OutDir>\n')
|
||||||
|
f.write(' <TargetName Condition="\'$(Configuration)|$(Platform)\'==\'Debug|Win32\'">%s</TargetName>\n' % name)
|
||||||
|
f.write(' <TargetExt Condition="\'$(Configuration)|$(Platform)\'==\'Debug|Win32\'">.%s</TargetExt>\n' % target_ext)
|
||||||
|
- f.write(' <OutDir Condition="\'$(Configuration)|$(Platform)\'==\'Release|Win32\'">$(SolutionDir)\$(ProjectName)\$(Configuration)\</OutDir>\n')
|
||||||
|
+ f.write(' <OutDir Condition="\'$(Configuration)|$(Platform)\'==\'Release|Win32\'">$(SolutionDir)\\$(ProjectName)\\$(Configuration)\\</OutDir>\n')
|
||||||
|
f.write(' <TargetName Condition="\'$(Configuration)|$(Platform)\'==\'Release|Win32\'">%s</TargetName>\n' % name)
|
||||||
|
f.write(' <TargetExt Condition="\'$(Configuration)|$(Platform)\'==\'Release|Win32\'">.%s</TargetExt>\n' % target_ext)
|
||||||
|
f.write(' </PropertyGroup>\n')
|
||||||
|
f.write(' <PropertyGroup Condition="\'$(Configuration)|$(Platform)\'==\'Debug|Win32\'">\n')
|
||||||
|
- f.write(' <IntDir>$(ProjectName)\$(Configuration)\</IntDir>\n')
|
||||||
|
+ f.write(' <IntDir>$(ProjectName)\\$(Configuration)\\</IntDir>\n')
|
||||||
|
f.write(' </PropertyGroup>\n')
|
||||||
|
f.write(' <PropertyGroup Condition="\'$(Configuration)|$(Platform)\'==\'Release|Win32\'">\n')
|
||||||
|
- f.write(' <IntDir>$(ProjectName)\$(Configuration)\</IntDir>\n')
|
||||||
|
+ f.write(' <IntDir>$(ProjectName)\\$(Configuration)\\</IntDir>\n')
|
||||||
|
f.write(' </PropertyGroup>\n')
|
||||||
|
|
||||||
|
|
||||||
|
@@ -3258,7 +3258,7 @@ def mk_vs_proj(name, components):
|
||||||
|
mk_vs_proj_link_exe(f, name, debug=False)
|
||||||
|
f.write(' </ItemDefinitionGroup>\n')
|
||||||
|
mk_vs_proj_dep_groups(f, name, components)
|
||||||
|
- f.write(' <Import Project="$(VCTargetsPath)\Microsoft.Cpp.targets" />\n')
|
||||||
|
+ f.write(' <Import Project="$(VCTargetsPath)\\Microsoft.Cpp.targets" />\n')
|
||||||
|
f.write(' <ImportGroup Label="ExtensionTargets">\n')
|
||||||
|
f.write(' </ImportGroup>\n')
|
||||||
|
f.write('</Project>\n')
|
||||||
|
@@ -3299,7 +3299,7 @@ def mk_vs_proj_dll(name, components):
|
||||||
|
mk_vs_proj_link_dll(f, name, debug=False)
|
||||||
|
f.write(' </ItemDefinitionGroup>\n')
|
||||||
|
mk_vs_proj_dep_groups(f, name, components)
|
||||||
|
- f.write(' <Import Project="$(VCTargetsPath)\Microsoft.Cpp.targets" />\n')
|
||||||
|
+ f.write(' <Import Project="$(VCTargetsPath)\\Microsoft.Cpp.targets" />\n')
|
||||||
|
f.write(' <ImportGroup Label="ExtensionTargets">\n')
|
||||||
|
f.write(' </ImportGroup>\n')
|
||||||
|
f.write('</Project>\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:
|
56
z3-ocaml.patch
Normal file
56
z3-ocaml.patch
Normal file
@ -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')
|
25
z3-stdint.patch
Normal file
25
z3-stdint.patch
Normal file
@ -0,0 +1,25 @@
|
|||||||
|
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<T>(((reinterpret_cast<uintptr_t>(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 ‘<cstdint>’; did you forget to ‘#include <cstdint>’?
|
||||||
|
56 | #include "util/page.h"
|
||||||
|
+++ |+#include <cstdint>
|
||||||
|
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 <cstdint>
|
||||||
|
#include "util/machine.h"
|
||||||
|
|
||||||
|
#define TAG_SHIFT PTR_ALIGNMENT
|
71
z3.spec
71
z3.spec
@ -7,23 +7,28 @@
|
|||||||
# unless somebody is really, really persuasive and available to help fix it
|
# unless somebody is really, really persuasive and available to help fix it
|
||||||
# if it breaks.
|
# if it breaks.
|
||||||
|
|
||||||
# Do not embed bad package note paths in the OCaml files.
|
|
||||||
%undefine _package_note_flags
|
|
||||||
|
|
||||||
# Tests are off by default because some of the tests require more memory than
|
# Tests are off by default because some of the tests require more memory than
|
||||||
# the koji builders have available.
|
# the koji builders have available.
|
||||||
%bcond_with test
|
%bcond_with test
|
||||||
|
|
||||||
Name: z3
|
Name: z3
|
||||||
Version: 4.12.1
|
Version: 4.12.2
|
||||||
Release: 2%{?dist}
|
Release: 7%{?dist}
|
||||||
Summary: Satisfiability Modulo Theories (SMT) solver
|
Summary: Satisfiability Modulo Theories (SMT) solver
|
||||||
|
|
||||||
License: MIT
|
License: MIT
|
||||||
URL: https://github.com/Z3Prover/z3
|
URL: https://github.com/Z3Prover/z3
|
||||||
Source0: https://github.com/Z3Prover/z3/archive/%{name}-%{version}.tar.gz
|
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
|
# 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
|
||||||
|
Patch2: %{name}-stdint.patch
|
||||||
|
# Fix malformed python escape sequences
|
||||||
|
# https://github.com/Z3Prover/z3/pull/6797
|
||||||
|
Patch3: %{name}-escapes.patch
|
||||||
|
|
||||||
BuildRequires: cmake
|
BuildRequires: cmake
|
||||||
BuildRequires: doxygen
|
BuildRequires: doxygen
|
||||||
@ -37,10 +42,12 @@ BuildRequires: javapackages-tools
|
|||||||
%endif
|
%endif
|
||||||
BuildRequires: make
|
BuildRequires: make
|
||||||
BuildRequires: ninja-build
|
BuildRequires: ninja-build
|
||||||
|
%ifnarch %{ix86}
|
||||||
BuildRequires: ocaml
|
BuildRequires: ocaml
|
||||||
BuildRequires: ocaml-findlib
|
BuildRequires: ocaml-findlib
|
||||||
BuildRequires: ocaml-ocamldoc
|
BuildRequires: ocaml-ocamldoc
|
||||||
BuildRequires: ocaml-zarith-devel
|
BuildRequires: ocaml-zarith-devel
|
||||||
|
%endif
|
||||||
BuildRequires: python3-devel
|
BuildRequires: python3-devel
|
||||||
BuildRequires: %{py3_dist setuptools}
|
BuildRequires: %{py3_dist setuptools}
|
||||||
|
|
||||||
@ -122,6 +129,8 @@ Requires: javapackages-tools
|
|||||||
Java interface to z3.
|
Java interface to z3.
|
||||||
%endif
|
%endif
|
||||||
|
|
||||||
|
# OCaml packages not built on i686 since OCaml 5 / Fedora 39.
|
||||||
|
%ifnarch %{ix86}
|
||||||
%package -n ocaml-z3
|
%package -n ocaml-z3
|
||||||
Summary: Ocaml interface to z3
|
Summary: Ocaml interface to z3
|
||||||
Requires: z3-libs%{?_isa} = %{version}-%{release}
|
Requires: z3-libs%{?_isa} = %{version}-%{release}
|
||||||
@ -136,6 +145,7 @@ Requires: ocaml-zarith-devel%{?_isa}
|
|||||||
|
|
||||||
%description -n ocaml-z3-devel
|
%description -n ocaml-z3-devel
|
||||||
Files for building ocaml applications that use z3.
|
Files for building ocaml applications that use z3.
|
||||||
|
%endif
|
||||||
|
|
||||||
%package -n python3-z3
|
%package -n python3-z3
|
||||||
Summary: Python 3 interface to z3
|
Summary: Python 3 interface to z3
|
||||||
@ -146,7 +156,11 @@ Requires: z3-libs = %{version}-%{release}
|
|||||||
Python 3 interface to z3.
|
Python 3 interface to z3.
|
||||||
|
|
||||||
%prep
|
%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,
|
# Enable verbose builds, use Fedora CFLAGS, preserve timestamps when installing,
|
||||||
# include the entire contents of the archives in the library, link the library
|
# include the entire contents of the archives in the library, link the library
|
||||||
@ -188,6 +202,7 @@ export PYTHON=%{python3}
|
|||||||
|
|
||||||
%cmake_build
|
%cmake_build
|
||||||
|
|
||||||
|
%ifnarch %{ix86}
|
||||||
# The cmake build system does not build the OCaml interface. Do that manually.
|
# The cmake build system does not build the OCaml interface. Do that manually.
|
||||||
#
|
#
|
||||||
# First, run the configure script to generate several files.
|
# First, run the configure script to generate several files.
|
||||||
@ -204,6 +219,7 @@ sed -i '/^api/s/ libz3\$(SO_EXT)//g' build/Makefile
|
|||||||
|
|
||||||
# Fourth, build the OCaml interface
|
# Fourth, build the OCaml interface
|
||||||
%make_build -C build ml
|
%make_build -C build ml
|
||||||
|
%endif
|
||||||
|
|
||||||
%install
|
%install
|
||||||
export LANG="C.UTF-8"
|
export LANG="C.UTF-8"
|
||||||
@ -220,13 +236,18 @@ ln -s %{_jnidir}/com.microsoft.z3.jar %{buildroot}%{_libdir}/z3
|
|||||||
mv %{buildroot}%{_libdir}/libz3java.so %{buildroot}%{_libdir}/z3
|
mv %{buildroot}%{_libdir}/libz3java.so %{buildroot}%{_libdir}/z3
|
||||||
%endif
|
%endif
|
||||||
|
|
||||||
|
%ifnarch %{ix86}
|
||||||
# Install the OCaml interface
|
# Install the OCaml interface
|
||||||
pushd build/api/ml
|
cd build/api/ml
|
||||||
mkdir -p %{buildroot}%{ocamldir}/Z3
|
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
|
mkdir -p %{buildroot}%{ocamldir}/stublibs
|
||||||
cp -p *.so %{buildroot}%{ocamldir}/stublibs
|
cp -p *.so %{buildroot}%{ocamldir}/stublibs
|
||||||
popd
|
cd -
|
||||||
|
%endif
|
||||||
|
|
||||||
# We handle the documentation files below
|
# We handle the documentation files below
|
||||||
rm -rf %{buildroot}%{_docdir}/Z3
|
rm -rf %{buildroot}%{_docdir}/Z3
|
||||||
@ -272,24 +293,54 @@ cd -
|
|||||||
%{_jnidir}/com.microsoft.z3*jar
|
%{_jnidir}/com.microsoft.z3*jar
|
||||||
%endif
|
%endif
|
||||||
|
|
||||||
|
%ifnarch %{ix86}
|
||||||
%files -n ocaml-z3
|
%files -n ocaml-z3
|
||||||
%dir %{ocamldir}/Z3/
|
%dir %{ocamldir}/Z3/
|
||||||
%{ocamldir}/Z3/META
|
%{ocamldir}/Z3/META
|
||||||
%{ocamldir}/Z3/*.cma
|
%{ocamldir}/Z3/*.cma
|
||||||
%{ocamldir}/Z3/*.cmi
|
%{ocamldir}/Z3/*.cmi
|
||||||
|
%ifarch %{ocaml_native_compiler}
|
||||||
%{ocamldir}/Z3/*.cmxs
|
%{ocamldir}/Z3/*.cmxs
|
||||||
|
%endif
|
||||||
%{ocamldir}/stublibs/*.so
|
%{ocamldir}/stublibs/*.so
|
||||||
|
|
||||||
%files -n ocaml-z3-devel
|
%files -n ocaml-z3-devel
|
||||||
%{ocamldir}/Z3/*.a
|
%{ocamldir}/Z3/*.a
|
||||||
|
%ifarch %{ocaml_native_compiler}
|
||||||
%{ocamldir}/Z3/*.cmx
|
%{ocamldir}/Z3/*.cmx
|
||||||
%{ocamldir}/Z3/*.cmxa
|
%{ocamldir}/Z3/*.cmxa
|
||||||
|
%endif
|
||||||
%{ocamldir}/Z3/*.mli
|
%{ocamldir}/Z3/*.mli
|
||||||
|
%endif
|
||||||
|
|
||||||
%files -n python3-z3
|
%files -n python3-z3
|
||||||
%{python3_sitelib}/z3/
|
%{python3_sitelib}/z3/
|
||||||
|
|
||||||
%changelog
|
%changelog
|
||||||
|
* Thu Oct 05 2023 Richard W.M. Jones <rjones@redhat.com> - 4.12.2-7
|
||||||
|
- OCaml 5.1 rebuild for Fedora 40
|
||||||
|
|
||||||
|
* Thu Jul 27 2023 Jerry James <loganjerry@gmail.com> - 4.12.2-6
|
||||||
|
- Rebuild for ocaml-zarith 1.13
|
||||||
|
|
||||||
|
* Sat Jul 22 2023 Fedora Release Engineering <releng@fedoraproject.org> - 4.12.2-5
|
||||||
|
- Rebuilt for https://fedoraproject.org/wiki/Fedora_39_Mass_Rebuild
|
||||||
|
|
||||||
|
* Fri Jul 21 2023 Jerry James <loganjerry@gmail.com> - 4.12.2-4
|
||||||
|
- Exclude the OCaml and Java subpackages only on i386
|
||||||
|
|
||||||
|
* Wed Jul 12 2023 Richard W.M. Jones <rjones@redhat.com> - 4.12.2-4
|
||||||
|
- OCaml 5.0 rebuild for Fedora 39
|
||||||
|
|
||||||
|
* Mon Jul 10 2023 Jerry James <loganjerry@gmail.com> - 4.12.2-3
|
||||||
|
- OCaml 5.0.0 rebuild
|
||||||
|
|
||||||
|
* Thu Jun 15 2023 Python Maint <python-maint@redhat.com> - 4.12.2-2
|
||||||
|
- Rebuilt for Python 3.12
|
||||||
|
|
||||||
|
* Mon May 15 2023 Jerry James <loganjerry@gmail.com> - 4.12.2-1
|
||||||
|
- Version 4.12.2
|
||||||
|
|
||||||
* Tue Jan 24 2023 Richard W.M. Jones <rjones@redhat.com> - 4.12.1-2
|
* Tue Jan 24 2023 Richard W.M. Jones <rjones@redhat.com> - 4.12.1-2
|
||||||
- Rebuild OCaml packages for F38
|
- Rebuild OCaml packages for F38
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user