From 6352149c0bbdc46ebb16088ccc094be1edb84692 Mon Sep 17 00:00:00 2001
From: Tai Chi Minh Ralph Eastwood <tcmreastwood@gmail.com>
Date: Mon, 8 Jan 2018 20:37:14 +0000
Subject: [PATCH] z3: z3-ocaml subpackage

---
 common/shlibs       |  1 +
 srcpkgs/z3-ocaml    |  1 +
 srcpkgs/z3/template | 32 ++++++++++++++++++++++++++++----
 3 files changed, 30 insertions(+), 4 deletions(-)
 create mode 120000 srcpkgs/z3-ocaml

diff --git a/common/shlibs b/common/shlibs
index a84c32ffc7..c6153f8bc7 100644
--- a/common/shlibs
+++ b/common/shlibs
@@ -3041,6 +3041,7 @@ libqmobipocket.so.2 libqmobipocket-17.04.3_1
 libgloox.so.17 gloox-1.0.20_1
 libgsmsd.so.8 gammu-smsd-1.39.0_1
 libGammu.so.8 gammu-1.39.0_1
+libz3.so z3-4.6.0_2
 libvulkan.so.1 vulkan-loader-1.0.57.0_1
 libVkLayer_core_validation.so vulkan-validation-layers-1.0.57.0_1
 libVkLayer_device_profile_api.so vulkan-validation-layers-1.0.57.0_1
diff --git a/srcpkgs/z3-ocaml b/srcpkgs/z3-ocaml
new file mode 120000
index 0000000000..e6b37640d8
--- /dev/null
+++ b/srcpkgs/z3-ocaml
@@ -0,0 +1 @@
+z3
\ No newline at end of file
diff --git a/srcpkgs/z3/template b/srcpkgs/z3/template
index bd1bd7ca97..aa6b129a45 100644
--- a/srcpkgs/z3/template
+++ b/srcpkgs/z3/template
@@ -1,10 +1,10 @@
 # Template file for 'z3'
 pkgname=z3
 version=4.6.0
-revision=1
+revision=2
 wrksrc="${pkgname}-${pkgname}-${version}"
-hostmakedepends="python"
-makedepends="libgomp-devel gmp-devel"
+hostmakedepends="python $(vopt_if ocaml 'ocaml ocaml-findlib')"
+makedepends="libgomp-devel gmp-devel $(vopt_if ocaml 'ocaml-num ncurses-devel')"
 depends="python python-setuptools"
 pycompile_module="z3"
 short_desc="Z3 theorem prover and SMT solver (command line + Python module)"
@@ -13,9 +13,14 @@ license="MIT"
 homepage="https://github.com/Z3Prover/z3"
 distfiles="https://github.com/Z3Prover/z3/archive/${pkgname}-${version}.tar.gz"
 checksum=511da31d1f985cf0c79b2de05bda4e057371ba519769d1546ff71e1304fe53c9
+build_options="ocaml"
+desc_option_ocaml="Enable support for OCaml bindings"
+build_options_default="ocaml"
+shlib_provides="libz3.so"
+subpackages="$(vopt_if ocaml z3-ocaml)"
 
 do_configure() {
-	LDFLAGS="$CFLAGS $LDFLAGS" ./configure --prefix=/usr -g
+	LDFLAGS="$CFLAGS $LDFLAGS" ./configure --prefix=/usr -g $(vopt_if ocaml --ml)
 }
 
 do_build() {
@@ -34,5 +39,24 @@ do_install() {
 	for f in build/python/z3/*; do
 		vinstall $f 0644 usr/lib/python2.7/site-packages/z3
 	done
+	if [ "$build_option_ocaml" ]; then
+		vmkdir usr/lib/ocaml/Z3
+		vinstall src/api/ml/z3.mli 0644 usr/lib/ocaml/Z3
+		for f in build/api/ml/*; do
+			case "$f" in
+				*.o)  continue ;;
+				*.so) vinstall $f 0644 usr/lib/ocaml/stublibs ;;
+				*)    vinstall $f 0644 usr/lib/ocaml/Z3
+			esac
+		done
+	fi
 	vlicense LICENSE.txt
 }
+
+z3-ocaml_package() {
+	short_desc="Z3 theorem prover and SMT solver (OCaml bindings)"
+	depends="z3>=${version}_${revision}"
+	pkg_install() {
+		vmove usr/lib/ocaml
+	}
+}