Compare commits
6 Commits
Author | SHA1 | Date | |
---|---|---|---|
|
dc29bbe7e3 | ||
|
7fc71e141c | ||
|
046bb852ea | ||
|
5ef0ea97d2 | ||
|
a628da3ca4 | ||
|
2a57573720 |
@ -1,5 +0,0 @@
|
|||||||
# z3
|
|
||||||
|
|
||||||
[Z3](https://github.com/Z3Prover/z3) is a theorem prover from Microsoft
|
|
||||||
Research. If you are not familiar with Z3, you can start
|
|
||||||
[here](https://github.com/Z3Prover/z3/wiki#background).
|
|
2
sources
2
sources
@ -1 +1 @@
|
|||||||
SHA512 (z3-4.12.4.tar.gz) = fcb778d2e3e0d13fc68afcd8724548279f9edbbb4aac1bbb93e00959c33330ab2fd84f2c2e4b0b78f767819725a90b845fc606a9adc931ae1f0a11f4deae433b
|
SHA512 (z3-4.8.9.tar.gz) = a50da5c3f9e27d3e804c1b71f648a3dbd5a55223b7344d66f191a1b34a4d787810abd976840d3ab3878aaf5c96d89f5a517cac0781b82aa927a9d8d54836d54f
|
||||||
|
@ -1,56 +0,0 @@
|
|||||||
--- 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')
|
|
21
z3-python.patch
Normal file
21
z3-python.patch
Normal file
@ -0,0 +1,21 @@
|
|||||||
|
--- 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 = []
|
25
z3.rpmlintrc
Normal file
25
z3.rpmlintrc
Normal file
@ -0,0 +1,25 @@
|
|||||||
|
# THIS FILE IS FOR WHITELISTING RPMLINT ERRORS AND WARNINGS IN TASKOTRON
|
||||||
|
# https://fedoraproject.org/wiki/Taskotron/Tasks/dist.rpmlint#Whitelisting_errors
|
||||||
|
|
||||||
|
# The dictionary is missing some technical terms
|
||||||
|
addFilter(r'W: spelling-error .* ((S|s)atisfiability|datatypes)')
|
||||||
|
|
||||||
|
# Shared objects in the python arch directory are not devel files
|
||||||
|
addFilter(r'python3-z3\.[^:]+: W: devel-file-in-non-devel-package .*libz3\.so')
|
||||||
|
|
||||||
|
# The documentation is in the -doc subpackage
|
||||||
|
addFilter(r'W: no-documentation')
|
||||||
|
|
||||||
|
# Oh yes, we have no manual page
|
||||||
|
addFilter(r'W: no-manual-page-for-binary z3')
|
||||||
|
|
||||||
|
# The configure script is not an autotools-generated script
|
||||||
|
addFilter(r'z3\.spec:[^:]*: W: configure-without-libdir-spec')
|
||||||
|
|
||||||
|
# The spec file moves the shared object from /usr/lib to /usr/lib64 on 64-bit
|
||||||
|
# systems, the opposite of the problem this warning is intended to catch.
|
||||||
|
addFilter(r'z3\.spec:[^:]+: E: hardcoded-library-path in %{_prefix}/lib/libz3\.so\*')
|
||||||
|
|
||||||
|
# This is where JAR files are supposed to go when there is a binary interface.
|
||||||
|
addFilter(r'z3\.spec:[^:]+: E: hardcoded-library-path in %{_prefix}/lib/\*\.jar')
|
||||||
|
addFilter(r'z3\.spec:[^:]+: E: hardcoded-library-path in %{_prefix}/lib/lib%{name}java\.so')
|
375
z3.spec
375
z3.spec
@ -1,26 +1,13 @@
|
|||||||
# TODO: A Julia interface is now available, but requires
|
|
||||||
# https://github.com/JuliaInterop/libcxxwrap-julia, which is not currently
|
|
||||||
# available in Fedora.
|
|
||||||
|
|
||||||
# TODO: A JavaScript interface is now available. Given the generally poor
|
|
||||||
# state of JavaScript in Fedora, I do not plan to add a subpackage for it
|
|
||||||
# unless somebody is really, really persuasive and available to help fix it
|
|
||||||
# if it breaks.
|
|
||||||
|
|
||||||
# Tests are off by default because some of the tests require more memory than
|
|
||||||
# the koji builders have available.
|
|
||||||
%bcond_with test
|
|
||||||
|
|
||||||
Name: z3
|
Name: z3
|
||||||
Version: 4.12.4
|
Version: 4.8.9
|
||||||
Release: 4%{?dist}
|
Release: 4%{?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
|
# Change the way python finds the shared object; see bz 1910923
|
||||||
Patch0: %{name}-ocaml.patch
|
Patch0: %{name}-python.patch
|
||||||
|
|
||||||
BuildRequires: cmake
|
BuildRequires: cmake
|
||||||
BuildRequires: doxygen
|
BuildRequires: doxygen
|
||||||
@ -28,18 +15,14 @@ BuildRequires: gcc-c++
|
|||||||
BuildRequires: gmp-devel
|
BuildRequires: gmp-devel
|
||||||
BuildRequires: graphviz
|
BuildRequires: graphviz
|
||||||
BuildRequires: help2man
|
BuildRequires: help2man
|
||||||
%ifarch %{java_arches}
|
|
||||||
BuildRequires: java-devel
|
BuildRequires: java-devel
|
||||||
BuildRequires: javapackages-tools
|
BuildRequires: javapackages-tools
|
||||||
%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}
|
||||||
|
|
||||||
@ -54,55 +37,17 @@ uninterpreted functions, and quantifiers.
|
|||||||
%package libs
|
%package libs
|
||||||
Summary: Library for applications that use z3 functionality
|
Summary: Library for applications that use z3 functionality
|
||||||
|
|
||||||
# This can be removed when F40 reaches EOL
|
|
||||||
%ifnarch %{java_arches}
|
|
||||||
Obsoletes: java-z3 < 4.8.17-5
|
|
||||||
%endif
|
|
||||||
|
|
||||||
%description libs
|
%description libs
|
||||||
Library for applications that use z3 functionality.
|
Library for applications that use z3 functionality.
|
||||||
|
|
||||||
%package devel
|
%package devel
|
||||||
Summary: Header files for build applications that use z3
|
Summary: Header files for build applications that use z3
|
||||||
Requires: z3-libs%{?_isa} = %{version}-%{release}
|
Requires: %{name}-libs%{?_isa} = %{version}-%{release}
|
||||||
|
|
||||||
%description devel
|
%description devel
|
||||||
Header files for build applications that use z3.
|
Header files for build applications that use z3.
|
||||||
|
|
||||||
%package doc
|
%package doc
|
||||||
# The content is MIT.
|
|
||||||
# Two files in examples are GPL-3.0-or-later WITH Bison-exception 2.2:
|
|
||||||
# examples/tptp/tptp5.tab.c
|
|
||||||
# examples/tptp/tptp5.tab.c
|
|
||||||
# Other licenses are due to files installed by doxygen.
|
|
||||||
# html/bc_s.png: GPL-1.0-or-later
|
|
||||||
# html/bdwn.png: GPL-1.0-or-later
|
|
||||||
# html/closed.png: GPL-1.0-or-later
|
|
||||||
# html/doc.png: GPL-1.0-or-later
|
|
||||||
# html/doxygen.css: GPL-1.0-or-later
|
|
||||||
# html/doxygen.svg: GPL-1.0-or-later
|
|
||||||
# html/dynsections.js: MIT
|
|
||||||
# html/folderclosed.png: GPL-1.0-or-later
|
|
||||||
# html/folderopen.png: GPL-1.0-or-later
|
|
||||||
# html/jquery.js: MIT
|
|
||||||
# html/nav_f.png: GPL-1.0-or-later
|
|
||||||
# html/nav_g.png: GPL-1.0-or-later
|
|
||||||
# html/nav_h.png: GPL-1.0-or-later
|
|
||||||
# html/open.png: GPL-1.0-or-later
|
|
||||||
# html/search/search.css: GPL-1.0-or-later
|
|
||||||
# html/search/search.js: MIT
|
|
||||||
# html/search/search_l.png: GPL-1.0-or-later
|
|
||||||
# html/search/search_m.png: GPL-1.0-or-later
|
|
||||||
# html/search/search_r.png: GPL-1.0-or-later
|
|
||||||
# html/splitbar.png: GPL-1.0-or-later
|
|
||||||
# html/sync_off.png: GPL-1.0-or-later
|
|
||||||
# html/sync_on.png: GPL-1.0-or-later
|
|
||||||
# html/tab_a.png: GPL-1.0-or-later
|
|
||||||
# html/tab_b.png: GPL-1.0-or-later
|
|
||||||
# html/tab_h.png: GPL-1.0-or-later
|
|
||||||
# html/tab_s.png: GPL-1.0-or-later
|
|
||||||
# html/tabs.css: GPL-1.0-or-later
|
|
||||||
License: MIT AND GPL-3.0-or-later WITH Bison-exception-2.2 AND GPL-1.0-or-later
|
|
||||||
Summary: API documentation for Z3
|
Summary: API documentation for Z3
|
||||||
# FIXME: this should be noarch, but we end up with different numbers of inheritance
|
# FIXME: this should be noarch, but we end up with different numbers of inheritance
|
||||||
# graphs on different architectures. Why?
|
# graphs on different architectures. Why?
|
||||||
@ -110,49 +55,39 @@ Summary: API documentation for Z3
|
|||||||
%description doc
|
%description doc
|
||||||
API documentation for Z3.
|
API documentation for Z3.
|
||||||
|
|
||||||
%ifarch %{java_arches}
|
%package -n java-%{name}
|
||||||
%package -n java-z3
|
|
||||||
Summary: Java interface to z3
|
Summary: Java interface to z3
|
||||||
Requires: z3-libs%{?_isa} = %{version}-%{release}
|
Requires: %{name}-libs%{?_isa} = %{version}-%{release}
|
||||||
Requires: java
|
Requires: java
|
||||||
Requires: javapackages-tools
|
Requires: javapackages-tools
|
||||||
|
|
||||||
%description -n java-z3
|
%description -n java-%{name}
|
||||||
Java interface to z3.
|
Java interface to z3.
|
||||||
%endif
|
|
||||||
|
|
||||||
# OCaml packages not built on i686 since OCaml 5 / Fedora 39.
|
%package -n ocaml-%{name}
|
||||||
%ifnarch %{ix86}
|
|
||||||
%package -n ocaml-z3
|
|
||||||
Summary: Ocaml interface to z3
|
Summary: Ocaml interface to z3
|
||||||
Requires: z3-libs%{?_isa} = %{version}-%{release}
|
Requires: %{name}-libs%{?_isa} = %{version}-%{release}
|
||||||
|
|
||||||
%description -n ocaml-z3
|
%description -n ocaml-%{name}
|
||||||
Ocaml interface to z3.
|
Ocaml interface to z3.
|
||||||
|
|
||||||
%package -n ocaml-z3-devel
|
%package -n ocaml-%{name}-devel
|
||||||
Summary: Files for building ocaml applications that use z3
|
Summary: Files for building ocaml applications that use z3
|
||||||
Requires: ocaml-z3%{?_isa} = %{version}-%{release}
|
Requires: ocaml-%{name}%{?_isa} = %{version}-%{release}
|
||||||
Requires: ocaml-zarith-devel%{?_isa}
|
|
||||||
|
|
||||||
%description -n ocaml-z3-devel
|
%description -n ocaml-%{name}-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-%{name}
|
||||||
Summary: Python 3 interface to z3
|
Summary: Python 3 interface to z3
|
||||||
BuildArch: noarch
|
BuildArch: noarch
|
||||||
Requires: z3-libs = %{version}-%{release}
|
Requires: %{name}-libs = %{version}-%{release}
|
||||||
|
|
||||||
%description -n python3-z3
|
%description -n python3-%{name}
|
||||||
Python 3 interface to z3.
|
Python 3 interface to z3.
|
||||||
|
|
||||||
%prep
|
%prep
|
||||||
%autosetup -N -n %{name}-%{name}-%{version}
|
%autosetup -p1 -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
|
||||||
@ -161,8 +96,8 @@ sed \
|
|||||||
-e 's/@$(CXX)/$(CXX)/' \
|
-e 's/@$(CXX)/$(CXX)/' \
|
||||||
-e '/O3/d' \
|
-e '/O3/d' \
|
||||||
-e "s/\(['\"]\)cp\([^[:alnum:]]\)/\1cp -p\2/" \
|
-e "s/\(['\"]\)cp\([^[:alnum:]]\)/\1cp -p\2/" \
|
||||||
-e "s/\(SLIBEXTRAFLAGS = '\)'/\1-Wl,--no-whole-archive'/" \
|
-e "s/\(SLIBEXTRAFLAGS = '\)'/\1-Wl,--no-whole-archive -Wl,--as-needed'/" \
|
||||||
-e '/SLIBFLAGS/s|-shared|& %{build_ldflags} -Wl,--whole-archive|' \
|
-e "/SLIBFLAGS/s|-shared|& $RPM_LD_FLAGS -Wl,--whole-archive|" \
|
||||||
-e 's/\(libz3$(SO_EXT)\)\(\\n\)/\1 -Wl,--no-whole-archive\2/' \
|
-e 's/\(libz3$(SO_EXT)\)\(\\n\)/\1 -Wl,--no-whole-archive\2/' \
|
||||||
-e "s/OCAML_FLAGS = ''/OCAML_FLAGS = '-g'/" \
|
-e "s/OCAML_FLAGS = ''/OCAML_FLAGS = '-g'/" \
|
||||||
-i scripts/mk_util.py
|
-i scripts/mk_util.py
|
||||||
@ -170,23 +105,30 @@ sed \
|
|||||||
# Comply with the Java packaging guidelines and fill in the version for python
|
# Comply with the Java packaging guidelines and fill in the version for python
|
||||||
majver=$(cut -d. -f-2 <<< %{version})
|
majver=$(cut -d. -f-2 <<< %{version})
|
||||||
sed -e '/libz3java/s,\(System\.load\)Library("\(.*\)"),\1("%{_libdir}/z3/\2.so"),' \
|
sed -e '/libz3java/s,\(System\.load\)Library("\(.*\)"),\1("%{_libdir}/z3/\2.so"),' \
|
||||||
-e "s/'so'/'so.$majver'/" \
|
-e "s/@MAJVER@/$majver/" \
|
||||||
-i scripts/update_api.py
|
-i scripts/update_api.py
|
||||||
|
|
||||||
# Turn off HTML timestamps for reproducible builds
|
# Update an OCaml interface
|
||||||
sed -i '/HTML_TIMESTAMP/s/YES/NO/' doc/z3api.cfg.in doc/z3code.dox
|
sed -i 's/Pervasives/Stdlib/' src/api/ml/z3.ml
|
||||||
|
|
||||||
|
# FIXME: For unknown reasons, cmake replaces the version with nothing at all
|
||||||
|
sed -i 's/@VERSION@/%{version}/' z3.pc.cmake.in
|
||||||
|
|
||||||
|
# Fix character encoding
|
||||||
|
iconv -f iso8859-1 -t utf-8 RELEASE_NOTES > RELEASE_NOTES.utf8
|
||||||
|
touch -r RELEASE_NOTES RELEASE_NOTES.utf8
|
||||||
|
mv -f RELEASE_NOTES.utf8 RELEASE_NOTES
|
||||||
|
|
||||||
%build
|
%build
|
||||||
export LANG=C.UTF-8
|
export CXXFLAGS="$RPM_OPT_FLAGS"
|
||||||
export PYTHON=%{python3}
|
export LANG="C.UTF-8"
|
||||||
|
export PYTHON="%{python3}"
|
||||||
|
|
||||||
%cmake -G Ninja \
|
%cmake -G Ninja \
|
||||||
-DCMAKE_INSTALL_INCLUDEDIR=%{_includedir}/z3 \
|
-DCMAKE_INSTALL_INCLUDEDIR=%{_includedir}/%{name} \
|
||||||
-DCMAKE_JAVA_COMPILE_FLAGS="-source;1.8;-target;1.8" \
|
-DCMAKE_JAVA_COMPILE_FLAGS="-source;1.8;-target;1.8" \
|
||||||
-DZ3_BUILD_DOCUMENTATION:BOOL=ON \
|
-DZ3_BUILD_DOCUMENTATION:BOOL=ON \
|
||||||
%ifarch %{java_arches}
|
|
||||||
-DZ3_BUILD_JAVA_BINDINGS:BOOL=ON \
|
-DZ3_BUILD_JAVA_BINDINGS:BOOL=ON \
|
||||||
%endif
|
|
||||||
-DZ3_BUILD_PYTHON_BINDINGS:BOOL=ON \
|
-DZ3_BUILD_PYTHON_BINDINGS:BOOL=ON \
|
||||||
-DZ3_INCLUDE_GIT_HASH:BOOL=OFF \
|
-DZ3_INCLUDE_GIT_HASH:BOOL=OFF \
|
||||||
-DZ3_INCLUDE_GIT_DESCRIBE:BOOL=OFF \
|
-DZ3_INCLUDE_GIT_DESCRIBE:BOOL=OFF \
|
||||||
@ -194,7 +136,6 @@ 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.
|
||||||
@ -211,7 +152,6 @@ 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"
|
||||||
@ -219,238 +159,78 @@ export LANG="C.UTF-8"
|
|||||||
# Install the C++, python3, and Java interfaces
|
# Install the C++, python3, and Java interfaces
|
||||||
%cmake_install
|
%cmake_install
|
||||||
|
|
||||||
%ifarch %{java_arches}
|
|
||||||
# Move the Java interface to its correct location
|
# Move the Java interface to its correct location
|
||||||
mkdir -p %{buildroot}%{_libdir}/z3
|
mkdir -p %{buildroot}%{_libdir}/%{name}
|
||||||
mkdir -p %{buildroot}%{_jnidir}
|
mkdir -p %{buildroot}%{_jnidir}
|
||||||
mv %{buildroot}%{_javadir}/*.jar %{buildroot}%{_jnidir}
|
mv %{buildroot}%{_javadir}/*.jar %{buildroot}%{_jnidir}
|
||||||
ln -s %{_jnidir}/com.microsoft.z3.jar %{buildroot}%{_libdir}/z3
|
ln -s %{_jnidir}/com.microsoft.z3.jar %{buildroot}%{_libdir}/%{name}
|
||||||
mv %{buildroot}%{_libdir}/libz3java.so %{buildroot}%{_libdir}/z3
|
mv %{buildroot}%{_libdir}/lib%{name}java.so %{buildroot}%{_libdir}/%{name}
|
||||||
%endif
|
|
||||||
|
|
||||||
%ifnarch %{ix86}
|
|
||||||
# Install the OCaml interface
|
# Install the OCaml interface
|
||||||
cd build/api/ml
|
pushd build/api/ml
|
||||||
mkdir -p %{buildroot}%{ocamldir}/Z3
|
mkdir -p %{buildroot}%{_libdir}/ocaml/Z3
|
||||||
%ifarch %{ocaml_native_compiler}
|
cp -p META *.{a,cma,cmi,cmx,cmxa,cmxs,mli} %{buildroot}%{_libdir}/ocaml/Z3
|
||||||
cp -p *.cmx{,a,s} %{buildroot}%{ocamldir}/Z3
|
mkdir -p %{buildroot}%{_libdir}/ocaml/stublibs
|
||||||
%endif
|
cp -p *.so %{buildroot}%{_libdir}/ocaml/stublibs
|
||||||
cp -p META *.{a,cma,cmi,mli} %{buildroot}%{ocamldir}/Z3
|
popd
|
||||||
mkdir -p %{buildroot}%{ocamldir}/stublibs
|
|
||||||
cp -p *.so %{buildroot}%{ocamldir}/stublibs
|
|
||||||
cd -
|
|
||||||
%endif
|
|
||||||
|
|
||||||
# We handle the documentation files below
|
# We handle the documentation files below
|
||||||
rm -rf %{buildroot}%{_docdir}/Z3
|
rm -rf %{buildroot}%{_docdir}/Z3
|
||||||
|
|
||||||
# Make a man page
|
# Make a man page
|
||||||
mkdir -p %{buildroot}%{_mandir}/man1
|
mkdir -p %{buildroot}%{_mandir}/man1
|
||||||
help2man -N -o %{buildroot}%{_mandir}/man1/z3.1 %{_vpath_builddir}/z3
|
help2man -N -o %{buildroot}%{_mandir}/man1/%{name}.1 %{_vpath_builddir}/%{name}
|
||||||
|
|
||||||
# Fix the pkgconfig file
|
#%%check
|
||||||
sed -i 's,//usr,,' %{buildroot}%{_libdir}/pkgconfig/z3.pc
|
# Some of the tests require more memory than the koji builders have available.
|
||||||
|
#
|
||||||
%if %{with test}
|
#export LANG="C.UTF-8"
|
||||||
%check
|
#pushd build
|
||||||
export LANG="C.UTF-8"
|
#make test-z3
|
||||||
cd build
|
#./test-z3 /a
|
||||||
make test-z3
|
#popd
|
||||||
./test-z3 /a
|
|
||||||
cd -
|
|
||||||
%endif
|
|
||||||
|
|
||||||
%files
|
%files
|
||||||
%doc README.md RELEASE_NOTES.md
|
%doc README.md RELEASE_NOTES
|
||||||
%{_bindir}/z3
|
%{_bindir}/%{name}
|
||||||
%{_mandir}/man1/z3.1*
|
%{_mandir}/man1/%{name}.1*
|
||||||
|
|
||||||
%files libs
|
%files libs
|
||||||
%license LICENSE.txt
|
%license LICENSE.txt
|
||||||
%{_libdir}/libz3.so.4.12*
|
%{_libdir}/lib%{name}.so.4*
|
||||||
|
|
||||||
%files devel
|
%files devel
|
||||||
%{_includedir}/z3/
|
%{_includedir}/%{name}/
|
||||||
%{_libdir}/libz3.so
|
%{_libdir}/lib%{name}.so
|
||||||
%{_libdir}/cmake/z3/
|
%{_libdir}/cmake/%{name}/
|
||||||
%{_libdir}/pkgconfig/z3.pc
|
%{_libdir}/pkgconfig/%{name}.pc
|
||||||
|
|
||||||
%files doc
|
%files doc
|
||||||
%doc %{_vpath_builddir}/doc/api/html examples
|
%doc %{_vpath_builddir}/doc/api/html examples
|
||||||
%license LICENSE.txt
|
%license LICENSE.txt
|
||||||
|
|
||||||
%ifarch %{java_arches}
|
%files -n java-%{name}
|
||||||
%files -n java-z3
|
%{_libdir}/%{name}/
|
||||||
%{_libdir}/z3/
|
|
||||||
%{_jnidir}/com.microsoft.z3*jar
|
%{_jnidir}/com.microsoft.z3*jar
|
||||||
%endif
|
|
||||||
|
|
||||||
%ifnarch %{ix86}
|
%files -n ocaml-%{name}
|
||||||
%files -n ocaml-z3
|
%dir %{_libdir}/ocaml/Z3/
|
||||||
%dir %{ocamldir}/Z3/
|
%{_libdir}/ocaml/Z3/META
|
||||||
%{ocamldir}/Z3/META
|
%{_libdir}/ocaml/Z3/*.cma
|
||||||
%{ocamldir}/Z3/*.cma
|
%{_libdir}/ocaml/Z3/*.cmi
|
||||||
%{ocamldir}/Z3/*.cmi
|
%{_libdir}/ocaml/Z3/*.cmxs
|
||||||
%ifarch %{ocaml_native_compiler}
|
%{_libdir}/ocaml/stublibs/*.so
|
||||||
%{ocamldir}/Z3/*.cmxs
|
|
||||||
%endif
|
|
||||||
%{ocamldir}/stublibs/*.so
|
|
||||||
|
|
||||||
%files -n ocaml-z3-devel
|
%files -n ocaml-%{name}-devel
|
||||||
%{ocamldir}/Z3/*.a
|
%{_libdir}/ocaml/Z3/*.a
|
||||||
%ifarch %{ocaml_native_compiler}
|
%{_libdir}/ocaml/Z3/*.cmx
|
||||||
%{ocamldir}/Z3/*.cmx
|
%{_libdir}/ocaml/Z3/*.cmxa
|
||||||
%{ocamldir}/Z3/*.cmxa
|
%{_libdir}/ocaml/Z3/*.mli
|
||||||
%endif
|
|
||||||
%{ocamldir}/Z3/*.mli
|
|
||||||
%endif
|
|
||||||
|
|
||||||
%files -n python3-z3
|
%files -n python3-%{name}
|
||||||
%{python3_sitelib}/z3/
|
%{python3_sitelib}/%{name}/
|
||||||
|
|
||||||
%changelog
|
%changelog
|
||||||
* Thu Dec 21 2023 Jerry James <loganjerry@gmail.com> - 4.12.4-4
|
|
||||||
- Fix python package library load name (bz 2255464)
|
|
||||||
|
|
||||||
* Mon Dec 18 2023 Richard W.M. Jones <rjones@redhat.com> - 4.12.4-3
|
|
||||||
- OCaml 5.1.1 + s390x code gen fix for Fedora 40
|
|
||||||
|
|
||||||
* Tue Dec 12 2023 Richard W.M. Jones <rjones@redhat.com> - 4.12.4-2
|
|
||||||
- OCaml 5.1.1 rebuild for Fedora 40
|
|
||||||
|
|
||||||
* Sat Dec 9 2023 Jerry James <loganjerry@gmail.com> - 4.12.4-1
|
|
||||||
- Version 4.12.4
|
|
||||||
- Drop upstreamed patches: python, stdint, escapes
|
|
||||||
|
|
||||||
* 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
|
|
||||||
- Rebuild OCaml packages for F38
|
|
||||||
|
|
||||||
* Sat Jan 21 2023 Jerry James <loganjerry@gmail.com> - 4.12.1-1
|
|
||||||
- Version 4.12.1
|
|
||||||
|
|
||||||
* Sat Jan 21 2023 Fedora Release Engineering <releng@fedoraproject.org> - 4.12.0-2
|
|
||||||
- Rebuilt for https://fedoraproject.org/wiki/Fedora_38_Mass_Rebuild
|
|
||||||
|
|
||||||
* Tue Jan 17 2023 Jerry James <loganjerry@gmail.com> - 4.12.0-1
|
|
||||||
- Version 4.12.0
|
|
||||||
- Drop upstreamed -data-race and -uninit patches
|
|
||||||
|
|
||||||
* Sun Jan 8 2023 Jerry James <loganjerry@gmail.com> - 4.11.2-2
|
|
||||||
- Add -data-race patch to fix segfault (bz 2157972)
|
|
||||||
- Add -uninit patch to fix use of an uninitialized value
|
|
||||||
|
|
||||||
* Wed Dec 14 2022 Jerry James <loganjerry@gmail.com> - 4.11.2-1
|
|
||||||
- Further clarify license of the doc subpackage (SPDX)
|
|
||||||
|
|
||||||
* Sun Sep 4 2022 Jerry James <loganjerry@gmail.com> - 4.11.2-1
|
|
||||||
- Version 4.11.2
|
|
||||||
|
|
||||||
* Fri Aug 19 2022 Jerry James <loganjerry@gmail.com> - 4.11.0-1
|
|
||||||
- Version 4.11.0
|
|
||||||
- Clarify license of the doc subpackage
|
|
||||||
|
|
||||||
* Mon Aug 8 2022 Jerry James <loganjerry@gmail.com> - 4.10.2-1
|
|
||||||
- Version 4.10.2
|
|
||||||
|
|
||||||
* Sat Jul 23 2022 Fedora Release Engineering <releng@fedoraproject.org> - 4.8.17-6
|
|
||||||
- Rebuilt for https://fedoraproject.org/wiki/Fedora_37_Mass_Rebuild
|
|
||||||
|
|
||||||
* Tue Jun 28 2022 Jerry James <loganjerry@gmail.com> - 4.8.17-5
|
|
||||||
- Do not support Java on i686 (rhbz#2104112)
|
|
||||||
- Use new OCaml macros
|
|
||||||
|
|
||||||
* Mon Jun 20 2022 Python Maint <python-maint@redhat.com> - 4.8.17-4
|
|
||||||
- Rebuilt for Python 3.11
|
|
||||||
|
|
||||||
* Sat Jun 18 2022 Richard W.M. Jones <rjones@redhat.com> - 4.8.17-3
|
|
||||||
- OCaml 4.14.0 rebuild
|
|
||||||
|
|
||||||
* Mon Jun 13 2022 Python Maint <python-maint@redhat.com> - 4.8.17-2
|
|
||||||
- Rebuilt for Python 3.11
|
|
||||||
|
|
||||||
* Mon May 16 2022 Jerry James <loganjerry@gmail.com> - 4.8.17-1
|
|
||||||
- Version 4.8.17
|
|
||||||
- Drop upstreamed -ambiguous-overload patch
|
|
||||||
|
|
||||||
* Thu Mar 24 2022 Jerry James <loganjerry@gmail.com> - 4.8.15-2
|
|
||||||
- Add -ambiguous-overload patch to fix cppcheck build failure
|
|
||||||
|
|
||||||
* Mon Mar 21 2022 Jerry James <loganjerry@gmail.com> - 4.8.15-1
|
|
||||||
- Version 4.8.15
|
|
||||||
|
|
||||||
* Sat Feb 05 2022 Jiri Vanek <jvanek@redhat.com> - 4.8.14-4
|
|
||||||
- Rebuilt for java-17-openjdk as system jdk
|
|
||||||
|
|
||||||
* Fri Feb 04 2022 Richard W.M. Jones <rjones@redhat.com> - 4.8.14-3
|
|
||||||
- OCaml 4.13.1 rebuild to remove package notes
|
|
||||||
|
|
||||||
* Sat Jan 22 2022 Fedora Release Engineering <releng@fedoraproject.org> - 4.8.14-2
|
|
||||||
- Rebuilt for https://fedoraproject.org/wiki/Fedora_36_Mass_Rebuild
|
|
||||||
|
|
||||||
* Fri Dec 24 2021 Jerry James <loganjerry@gmail.com> - 4.8.14-1
|
|
||||||
- Version 4.8.14
|
|
||||||
- Conditionalize the %%check script
|
|
||||||
|
|
||||||
* Fri Nov 19 2021 Jerry James <loganjerry@gmail.com> - 4.8.13-1
|
|
||||||
- Version 4.8.13
|
|
||||||
|
|
||||||
* Mon Oct 04 2021 Richard W.M. Jones <rjones@redhat.com> - 4.8.12-3
|
|
||||||
- OCaml 4.13.1 build
|
|
||||||
|
|
||||||
* Fri Jul 23 2021 Fedora Release Engineering <releng@fedoraproject.org> - 4.8.12-2
|
|
||||||
- Rebuilt for https://fedoraproject.org/wiki/Fedora_35_Mass_Rebuild
|
|
||||||
|
|
||||||
* Tue Jul 13 2021 Jerry James <loganjerry@gmail.com> - 4.8.12-1
|
|
||||||
- Version 4.8.12
|
|
||||||
|
|
||||||
* Sun Jun 6 2021 Jerry James <loganjerry@gmail.com> - 4.8.11-1
|
|
||||||
- Version 4.8.11
|
|
||||||
|
|
||||||
* Fri Jun 04 2021 Python Maint <python-maint@redhat.com> - 4.8.10-6
|
|
||||||
- Rebuilt for Python 3.10
|
|
||||||
|
|
||||||
* Wed Mar 3 2021 Jerry James <loganjerry@gmail.com> - 4.8.10-5
|
|
||||||
- Rebuild for ocaml-zarith 1.12
|
|
||||||
|
|
||||||
* Mon Mar 1 20:17:48 GMT 2021 Richard W.M. Jones <rjones@redhat.com> - 4.8.10-4
|
|
||||||
- Bump release and rebuild.
|
|
||||||
|
|
||||||
* Mon Mar 1 19:41:16 GMT 2021 Richard W.M. Jones <rjones@redhat.com> - 4.8.10-3
|
|
||||||
- Bump release and rebuild.
|
|
||||||
|
|
||||||
* Mon Mar 1 16:57:45 GMT 2021 Richard W.M. Jones <rjones@redhat.com> - 4.8.10-2
|
|
||||||
- OCaml 4.12.0 build
|
|
||||||
|
|
||||||
* Sat Feb 13 2021 Jerry James <loganjerry@gmail.com> - 4.8.10-1
|
|
||||||
- Version 4.8.10
|
|
||||||
|
|
||||||
* Thu Jan 28 2021 Fedora Release Engineering <releng@fedoraproject.org> - 4.8.9-5
|
|
||||||
- Rebuilt for https://fedoraproject.org/wiki/Fedora_34_Mass_Rebuild
|
|
||||||
|
|
||||||
* Fri Dec 25 2020 Jerry James <loganjerry@gmail.com> - 4.8.9-4
|
* Fri Dec 25 2020 Jerry James <loganjerry@gmail.com> - 4.8.9-4
|
||||||
- Fix the python interface (bz 1910923)
|
- Fix the python interface (bz 1910923)
|
||||||
|
|
||||||
@ -463,6 +243,9 @@ cd -
|
|||||||
* Fri Sep 11 2020 Jerry James <loganjerry@gmail.com> - 4.8.9-1
|
* Fri Sep 11 2020 Jerry James <loganjerry@gmail.com> - 4.8.9-1
|
||||||
- Version 4.8.9
|
- Version 4.8.9
|
||||||
|
|
||||||
|
* Wed Sep 02 2020 Richard W.M. Jones <rjones@redhat.com> - 4.8.8-7.1
|
||||||
|
- Bump release and rebuild.
|
||||||
|
|
||||||
* Tue Sep 01 2020 Richard W.M. Jones <rjones@redhat.com> - 4.8.8-7
|
* Tue Sep 01 2020 Richard W.M. Jones <rjones@redhat.com> - 4.8.8-7
|
||||||
- OCaml 4.11.1 rebuild
|
- OCaml 4.11.1 rebuild
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user