[packages/z3] - updated to 4.8.7 - ocaml interface now uses zarith instead of num

qboosh qboosh at pld-linux.org
Sat Dec 28 08:23:03 CET 2019


commit 01b2836f2e38844dc3504930203719521869b76d
Author: Jakub Bogusz <qboosh at pld-linux.org>
Date:   Sat Dec 28 08:23:50 2019 +0100

    - updated to 4.8.7
    - ocaml interface now uses zarith instead of num

 z3.spec | 49 ++++++++++++++++++++++++++-----------------------
 1 file changed, 26 insertions(+), 23 deletions(-)
---
diff --git a/z3.spec b/z3.spec
index 01de73b..32a388b 100644
--- a/z3.spec
+++ b/z3.spec
@@ -13,13 +13,13 @@
 Summary:	High-performance theorem prover developed at Microsoft Research
 Summary(pl.UTF-8):	Wydajne narzędzie do dowodzenia twierdzeń tworzone przez Microsoft Research
 Name:		z3
-Version:	4.8.5
+Version:	4.8.7
 Release:	1
 License:	MIT
 Group:		Applications/Engineering
 #Source0Download: https://github.com/Z3Prover/z3/releases
-Source0:	https://github.com/Z3Prover/z3/archive/Z3-%{version}.tar.gz
-# Source0-md5:	2095a1a6ebdae2a50c0c9b801292ff24
+Source0:	https://github.com/Z3Prover/z3/archive/z3-%{version}.tar.gz
+# Source0-md5:	18e7332ab136c1d8686ea719ed7107ed
 Patch0:		%{name}-pld.patch
 URL:		https://github.com/Z3Prover/z3
 BuildRequires:	cmake >= 3.4
@@ -31,6 +31,7 @@ BuildRequires:	libstdc++-devel >= 6:4.7
 %if %{with ocaml}
 BuildRequires:	ocaml
 BuildRequires:	ocaml-findlib
+BuildRequires:	ocaml-zarith-devel
 %endif
 BuildRequires:	python
 BuildRoot:	%{tmpdir}/%{name}-%{version}-root-%(id -u -n)
@@ -86,6 +87,7 @@ Summary:	Z3 binding for OCaml
 Summary(pl.UTF-8):	Wiązania Z3 dla OCamla
 Group:		Libraries
 Requires:	%{name} = %{version}-%{release}
+Requires:	ocaml-zarith
 %requires_eq	ocaml-runtime
 
 %description -n ocaml-z3
@@ -101,6 +103,7 @@ Summary:	Z3 binding for OCaml - development part
 Summary(pl.UTF-8):	Wiązania Z3 dla OCamla - cześć programistyczna
 Group:		Development/Libraries
 Requires:	ocaml-z3 = %{version}-%{release}
+Requires:	ocaml-zarith-devel
 %requires_eq	ocaml
 
 %description -n ocaml-z3-devel
@@ -124,7 +127,7 @@ Python API for Z3 theorem prover library.
 API języka Python do biblioteki dowodzenia twierdzeń Z3.
 
 %prep
-%setup -q -n z3-Z3-%{version}
+%setup -q -n z3-z3-%{version}
 %patch0 -p1
 
 %build
@@ -163,18 +166,18 @@ OCAMLOPT=ocamlc \
 install -d build-cmake
 cd build-cmake
 %cmake .. \
-	%{?with_apidocs:-DBUILD_DOCUMENTATION=ON} \
-	-DBUILD_LIBZ3_SHARED=ON \
-	%{?with_dotnet:-DBUILD_DOTNET_BINDINGS=ON} \
-	-DBUILD_JAVA_BINDINGS=ON \
-	-DBUILD_PYTHON_BINDINGS=ON \
 	-DCMAKE_INSTALL_INCLUDEDIR=%{_includedir}/z3 \
 	-DCMAKE_INSTALL_PYTHON_PKG_DIR=%{py_sitescriptdir} \
 	%{?with_dotnet:-DINSTALL_DOTNET_BINDINGS=ON} \
 	-DINSTALL_JAVA_BINDINGS=ON \
 	-DINSTALL_PYTHON_BINDINGS=ON \
 	-DUSE_LIB_GMP=ON \
-	-DUSE_OPENMP=ON
+	-DUSE_OPENMP=ON \
+	%{?with_apidocs:-DZ3_BUILD_DOCUMENTATION=ON} \
+	%{?with_dotnet:-DZ3_BUILD_DOTNET_BINDINGS=ON} \
+	-DZ3_BUILD_JAVA_BINDINGS=ON \
+	-DZ3_BUILD_LIBZ3_SHARED=ON \
+	-DZ3_BUILD_PYTHON_BINDINGS=ON
 
 %{__make}
 
@@ -182,23 +185,23 @@ cd build-cmake
 # no cmake suite for ocaml; do it manually (basing on Makefile generated by mk_make.py)
 install -d src/api/ml
 cp -p ../build/api/ml/META src/api/ml
-ocamlfind ocamlc -package num -ccopt "%{rpmcxxflags} -I../src/api -I../src/api/ml -o src/api/ml/z3native_stubs.o" -c ../src/api/ml/z3native_stubs.c
-ocamlfind ocamlc -package num -i -I src/api/ml -c ../src/api/ml/z3enums.ml > src/api/ml/z3enums.mli
-ocamlfind ocamlc -package num -I src/api/ml -o src/api/ml/z3enums.cmi -c src/api/ml/z3enums.mli
-ocamlfind ocamlc -package num -I src/api/ml -o src/api/ml/z3enums.cmo -c ../src/api/ml/z3enums.ml
-ocamlfind ocamlc -package num -i -I src/api/ml -o ../src/api/ml/z3native.ml > src/api/ml/z3native.mli
-ocamlfind ocamlc -package num -I src/api/ml -o src/api/ml/z3native.cmi -c src/api/ml/z3native.mli
-ocamlfind ocamlc -package num -I src/api/ml -o src/api/ml/z3native.cmo -c ../src/api/ml/z3native.ml
+ocamlfind ocamlc -package zarith -ccopt "%{rpmcxxflags} -I../src/api -I../src/api/ml -o src/api/ml/z3native_stubs.o" -c ../src/api/ml/z3native_stubs.c
+ocamlfind ocamlc -package zarith -i -I src/api/ml -c ../src/api/ml/z3enums.ml > src/api/ml/z3enums.mli
+ocamlfind ocamlc -package zarith -I src/api/ml -o src/api/ml/z3enums.cmi -c src/api/ml/z3enums.mli
+ocamlfind ocamlc -package zarith -I src/api/ml -o src/api/ml/z3enums.cmo -c ../src/api/ml/z3enums.ml
+ocamlfind ocamlc -package zarith -i -I src/api/ml -o ../src/api/ml/z3native.ml > src/api/ml/z3native.mli
+ocamlfind ocamlc -package zarith -I src/api/ml -o src/api/ml/z3native.cmi -c src/api/ml/z3native.mli
+ocamlfind ocamlc -package zarith -I src/api/ml -o src/api/ml/z3native.cmo -c ../src/api/ml/z3native.ml
 cp -p ../src/api/ml/z3.mli src/api/ml/z3.mli
-ocamlfind ocamlc -package num -I src/api/ml -o src/api/ml/z3.cmi -c src/api/ml/z3.mli
-ocamlfind ocamlc -package num -I src/api/ml -o src/api/ml/z3.cmo -c ../src/api/ml/z3.ml
+ocamlfind ocamlc -package zarith -I src/api/ml -o src/api/ml/z3.cmi -c src/api/ml/z3.mli
+ocamlfind ocamlc -package zarith -I src/api/ml -o src/api/ml/z3.cmo -c ../src/api/ml/z3.ml
 ocamlmklib -o src/api/ml/z3ml -I src/api/ml src/api/ml/z3native_stubs.o src/api/ml/z3enums.cmo src/api/ml/z3native.cmo src/api/ml/z3.cmo -cclib -lz3 -cclib -fopenmp
 %if %{with ocaml_opt}
-ocamlfind ocamlopt -package num -I src/api/ml -o src/api/ml/z3enums.cmx -c ../src/api/ml/z3enums.ml
-ocamlfind ocamlopt -package num -I src/api/ml -o src/api/ml/z3native.cmx -c ../src/api/ml/z3native.ml
-ocamlfind ocamlopt -package num -I src/api/ml -o src/api/ml/z3.cmx -c ../src/api/ml/z3.ml
+ocamlfind ocamlopt -package zarith -I src/api/ml -o src/api/ml/z3enums.cmx -c ../src/api/ml/z3enums.ml
+ocamlfind ocamlopt -package zarith -I src/api/ml -o src/api/ml/z3native.cmx -c ../src/api/ml/z3native.ml
+ocamlfind ocamlopt -package zarith -I src/api/ml -o src/api/ml/z3.cmx -c ../src/api/ml/z3.ml
 ocamlmklib -o src/api/ml/z3ml -I src/api/ml src/api/ml/z3native_stubs.o src/api/ml/z3enums.cmx src/api/ml/z3native.cmx src/api/ml/z3.cmx -cclib -lz3 -cclib -fopenmp
-ocamlfind ocamlopt -package num -linkall -shared -o src/api/ml/z3ml.cmxs -I . -I src/api/ml src/api/ml/z3ml.cmxa
+ocamlfind ocamlopt -package zarith -linkall -shared -o src/api/ml/z3ml.cmxs -I . -I src/api/ml src/api/ml/z3ml.cmxa
 %endif
 %endif
 
================================================================

---- gitweb:

http://git.pld-linux.org/gitweb.cgi/packages/z3.git/commitdiff/01b2836f2e38844dc3504930203719521869b76d



More information about the pld-cvs-commit mailing list