math/why3-spark: Upgrade version 2015 => 2016 (unbreaks)

6 files changed, 42 insertions, 99 deletions

diff --git a/math/why3-spark/Makefile b/math/why3-spark/Makefile
index 4a271a1b7771..e584cd0c2311 100644
--- a/math/why3-spark/Makefile
+++ b/math/why3-spark/Makefile
@@ -2,10 +2,9 @@
 # $FreeBSD$
 
 PORTNAME=	why3
-PORTVERSION=	2015
+PORTVERSION=	2016
 CATEGORIES=	math
-MASTER_SITES=	http://downloads.dragonlace.net/src/ \
-		LOCAL/marino
+MASTER_SITES=	http://downloads.dragonlace.net/src/
 PKGNAMESUFFIX=	-spark
 DISTNAME=	why3-for-spark-gpl-${PORTVERSION}-src
 
@@ -15,8 +14,6 @@ COMMENT=	Component of SPARK 2015
 LICENSE=	LGPL21 GPLv3
 LICENSE_COMB=	multi
 
-BROKEN=		broken by recent updated to an ocaml dependency
-
 BUILD_DEPENDS=	menhir:devel/menhir \
 		ocaml-zip>1:archivers/ocaml-zip \
 		ocaml-zarith>1.2:math/ocaml-zarith \
@@ -24,9 +21,12 @@ BUILD_DEPENDS=	menhir:devel/menhir \
 		ocaml-sqlite3>2:databases/ocaml-sqlite3 \
 		ocaml-ocamlgraph>1.8:math/ocaml-ocamlgraph \
 		camlp5o:devel/ocaml-camlp5
+LIB_DEPENDS=	libfontconfig.so:x11-fonts/fontconfig \
+		libfreetype.so:print/freetype2
 
-USES=		gmake
+USES=		gmake gettext
 USE_OCAML=	yes
+USE_GNOME=	gtk20 pango atk cairo gdkpixbuf2 glib20 gtksourceview2
 ALL_TARGET=	all
 GNU_CONFIGURE=	yes
 INSTALL_TARGET=	install-all
@@ -45,6 +45,13 @@ post-patch:
 	@${REINPLACE_CMD} -e 's|/bin/bash|/bin/sh|g' \
 		${WRKSRC}/src/util/sysutil.ml
 	@${REINPLACE_CMD} -e '/cp -f share\/Make/d' \
-		-e 's|why3.el|why3-mode.el|' ${WRKSRC}/Makefile.in
+		${WRKSRC}/Makefile.in
+
+post-install:
+	${STRIP_CMD} ${STAGEDIR}${PREFIX}/bin/*why3
+	${STRIP_CMD} ${STAGEDIR}${PREFIX}/lib/why3/why3server
+	${STRIP_CMD} ${STAGEDIR}${PREFIX}/lib/why3/why3cpulimit
+	${STRIP_CMD} ${STAGEDIR}${PREFIX}/lib/why3/commands/why3*
+	${STRIP_CMD} ${STAGEDIR}${PREFIX}/lib/why3/plugins/*.cmxs
 
 .include <bsd.port.mk>
diff --git a/math/why3-spark/distinfo b/math/why3-spark/distinfo
index 2a3be98e5d50..a87c9d776823 100644
--- a/math/why3-spark/distinfo
+++ b/math/why3-spark/distinfo
@@ -1,2 +1,3 @@
-SHA256 (why3-for-spark-gpl-2015-src.tar.gz) = 90faf6001e4a9d9ccb7c913df8a2316bef004aaf9546a9a5ff6b08c28ff74ede
-SIZE (why3-for-spark-gpl-2015-src.tar.gz) = 6880072
+TIMESTAMP = 1465729881
+SHA256 (why3-for-spark-gpl-2016-src.tar.gz) = 09e1161d7ff4a1974ff22a2e09d4ceb2ab125d6de4863c13371e212e0e50b19c
+SIZE (why3-for-spark-gpl-2016-src.tar.gz) = 8740369
diff --git a/math/why3-spark/files/patch-Makefile.in b/math/why3-spark/files/patch-Makefile.in
deleted file mode 100644
index 9c962d3cea78..000000000000
--- a/math/why3-spark/files/patch-Makefile.in
+++ /dev/null
@@ -1,26 +0,0 @@
---- Makefile.in.orig	2015-06-26 21:21:27 UTC
-+++ Makefile.in
-@@ -45,7 +45,6 @@ OCAMLLIB  = @OCAMLLIB@
- OCAMLINSTALLLIB  = $(DESTDIR)@OCAMLINSTALLLIB@
- OCAMLBEST = @OCAMLBEST@
- OCAMLVERSION = @OCAMLVERSION@
--CC        = gcc
- COQC      = @COQC@
- COQDEP    = @COQDEP@
- CAMLP5O   = @CAMLP5O@
-@@ -638,12 +637,12 @@ SERVER_O:= $(addprefix src/tools/, $(add
- opt: bin/why3server$(EXE)
- 
- bin/why3server$(EXE): $(SERVER_O)
--	gcc -o $@ $^
-+	$(CC) -o $@ $^
- 
- %.o: %.c %.h
--	gcc -c -Wall -g -o $@ $<
-+	$(CC) -c -Wall -g -o $@ $<
- %.o: %.c
--	gcc -c -Wall -g -o $@ $<
-+	$(CC) -c -Wall -g -o $@ $<
- 
- src/tools/main.o:: src/tools/server-unix.c src/tools/server-win.c
- 
diff --git a/math/why3-spark/files/patch-src_tools_cpulimit.c b/math/why3-spark/files/patch-src_tools_cpulimit.c
deleted file mode 100644
index f10f73f2aff3..000000000000
--- a/math/why3-spark/files/patch-src_tools_cpulimit.c
+++ /dev/null
@@ -1,10 +0,0 @@
---- src/tools/cpulimit.c.orig	2015-05-06 10:55:30 UTC
-+++ src/tools/cpulimit.c
-@@ -19,6 +19,7 @@
- #include <unistd.h>
- #include <signal.h>
- #include <errno.h>
-+#include <signal.h>
- #include <string.h>
- #include <sys/wait.h>
- 
diff --git a/math/why3-spark/pkg-descr b/math/why3-spark/pkg-descr
index c6a8b3de3be8..7b206e0de540 100644
--- a/math/why3-spark/pkg-descr
+++ b/math/why3-spark/pkg-descr
@@ -1,5 +1,5 @@
-This is a component of SPARK 2014.  Those looking for the deductive
+This is a component of SPARK 2016.  Those looking for the deductive
 program verification platform known as why3 should refer to math/why3
 instead.
 
-WWW: https://forge.open-do.org/projects/spark2014
+WWW: http://www.spark-2014.org/
diff --git a/math/why3-spark/pkg-plist b/math/why3-spark/pkg-plist
index a85c8ed25d60..ef92ed0ef05e 100644
--- a/math/why3-spark/pkg-plist
+++ b/math/why3-spark/pkg-plist
@@ -1,7 +1,5 @@
 bin/gnatwhy3
 bin/why3
-bin/why3-cpulimit
-bin/why3server
 %%OCAML_SITELIBDIR%%/why3/META
 %%OCAML_SITELIBDIR%%/why3/why3.a
 %%OCAML_SITELIBDIR%%/why3/why3.cmi
@@ -26,11 +24,11 @@ lib/why3/plugins/genequlin.cmxs
 lib/why3/plugins/hypothesis_selection.cmxs
 lib/why3/plugins/tptp.cmxs
 lib/why3/why3-call-pvs
+lib/why3/why3cpulimit
+lib/why3/why3server
 share/emacs/site-lisp/why3.el
 %%DATADIR%%/LICENSE
 %%DATADIR%%/drivers/alt_ergo.drv
-%%DATADIR%%/drivers/alt_ergo_0.93.drv
-%%DATADIR%%/drivers/alt_ergo_0.94.drv
 %%DATADIR%%/drivers/alt_ergo_common.drv
 %%DATADIR%%/drivers/alt_ergo_model.drv
 %%DATADIR%%/drivers/alt_ergo_smt2.drv
@@ -38,39 +36,48 @@ share/emacs/site-lisp/why3.el
 %%DATADIR%%/drivers/coq-common.gen
 %%DATADIR%%/drivers/coq-realizations.aux
 %%DATADIR%%/drivers/coq-realize.drv
+%%DATADIR%%/drivers/coq-ssreflect.drv
 %%DATADIR%%/drivers/coq.drv
 %%DATADIR%%/drivers/cvc3.drv
-%%DATADIR%%/drivers/cvc3_bare.drv
+%%DATADIR%%/drivers/cvc4-realize.drv
 %%DATADIR%%/drivers/cvc4.drv
 %%DATADIR%%/drivers/cvc4_14.drv
 %%DATADIR%%/drivers/cvc4_15.drv
-%%DATADIR%%/drivers/cvc4_bare.drv
 %%DATADIR%%/drivers/cvc4_bv.gen
 %%DATADIR%%/drivers/cvc4_gnatprove.drv
+%%DATADIR%%/drivers/cvc4_gnatprove_ce.drv
 %%DATADIR%%/drivers/discrimination.gen
 %%DATADIR%%/drivers/eprover.drv
 %%DATADIR%%/drivers/gappa.drv
 %%DATADIR%%/drivers/iprover.drv
+%%DATADIR%%/drivers/isabelle-2015.gen
+%%DATADIR%%/drivers/isabelle-2016.gen
 %%DATADIR%%/drivers/isabelle-common.gen
 %%DATADIR%%/drivers/isabelle-realizations.aux
-%%DATADIR%%/drivers/isabelle-realize.drv
-%%DATADIR%%/drivers/isabelle.drv
+%%DATADIR%%/drivers/isabelle2015-realize.drv
+%%DATADIR%%/drivers/isabelle2015.drv
+%%DATADIR%%/drivers/isabelle2016-realize.drv
+%%DATADIR%%/drivers/isabelle2016.drv
 %%DATADIR%%/drivers/mathematica.drv
 %%DATADIR%%/drivers/mathsat.drv
 %%DATADIR%%/drivers/metis.drv
 %%DATADIR%%/drivers/metitarski.drv
+%%DATADIR%%/drivers/no-bv.gen
 %%DATADIR%%/drivers/ocaml-gen.drv
 %%DATADIR%%/drivers/ocaml-no-arith.drv
 %%DATADIR%%/drivers/ocaml-unsafe-int.drv
 %%DATADIR%%/drivers/ocaml32.drv
 %%DATADIR%%/drivers/ocaml64.drv
+%%DATADIR%%/drivers/polypaver.drv
 %%DATADIR%%/drivers/princess.drv
 %%DATADIR%%/drivers/psyche.drv
 %%DATADIR%%/drivers/pvs-common.gen
 %%DATADIR%%/drivers/pvs-realizations.aux
 %%DATADIR%%/drivers/pvs-realize.drv
 %%DATADIR%%/drivers/pvs.drv
+%%DATADIR%%/drivers/safeprover.drv
 %%DATADIR%%/drivers/simplify.drv
+%%DATADIR%%/drivers/smt-libv2-bv-realization.gen
 %%DATADIR%%/drivers/smt-libv2-bv.gen
 %%DATADIR%%/drivers/smt-libv2.drv
 %%DATADIR%%/drivers/spass.drv
@@ -85,44 +92,15 @@ share/emacs/site-lisp/why3.el
 %%DATADIR%%/drivers/why3_tptp.drv
 %%DATADIR%%/drivers/yices-smt2.drv
 %%DATADIR%%/drivers/yices.drv
-%%DATADIR%%/drivers/yices_bare.drv
+%%DATADIR%%/drivers/z3-realize.drv
 %%DATADIR%%/drivers/z3.drv
 %%DATADIR%%/drivers/z3_432.drv
+%%DATADIR%%/drivers/z3_440.drv
+%%DATADIR%%/drivers/z3_gnatprove.drv
 %%DATADIR%%/drivers/z3_smtv1.drv
 %%DATADIR%%/drivers/zenon.drv
-%%DATADIR%%/images/boomy/accept32.png
-%%DATADIR%%/images/boomy/bug32.png
-%%DATADIR%%/images/boomy/clock32.png
-%%DATADIR%%/images/boomy/configure16.png
-%%DATADIR%%/images/boomy/configure32.png
-%%DATADIR%%/images/boomy/cut32.png
-%%DATADIR%%/images/boomy/cutb32.png
-%%DATADIR%%/images/boomy/delete32.png
-%%DATADIR%%/images/boomy/deletefile32.png
-%%DATADIR%%/images/boomy/edit32.png
-%%DATADIR%%/images/boomy/file16.png
-%%DATADIR%%/images/boomy/file32.png
-%%DATADIR%%/images/boomy/folder16.png
-%%DATADIR%%/images/boomy/folder32.png
-%%DATADIR%%/images/boomy/help32.png
-%%DATADIR%%/images/boomy/license.txt
-%%DATADIR%%/images/boomy/movefile32.png
-%%DATADIR%%/images/boomy/obsaccept32.png
-%%DATADIR%%/images/boomy/obsbug32.png
-%%DATADIR%%/images/boomy/obsclock32.png
-%%DATADIR%%/images/boomy/obsdelete32.png
-%%DATADIR%%/images/boomy/obsdeletefile32.png
-%%DATADIR%%/images/boomy/obshelp32.png
-%%DATADIR%%/images/boomy/pause32.png
-%%DATADIR%%/images/boomy/pausehalf32.png
-%%DATADIR%%/images/boomy/play32.png
-%%DATADIR%%/images/boomy/refresh32.png
-%%DATADIR%%/images/boomy/stop32.png
-%%DATADIR%%/images/boomy/transformation32.png
-%%DATADIR%%/images/boomy/trashb32.png
-%%DATADIR%%/images/boomy/undone32.png
-%%DATADIR%%/images/boomy/wizard16.png
-%%DATADIR%%/images/boomy/wizard32.png
+%%DATADIR%%/drivers/zenon_modulo.drv
+%%DATADIR%%/images/fatcow.rc
 %%DATADIR%%/images/fatcow/accept.png
 %%DATADIR%%/images/fatcow/bin.png
 %%DATADIR%%/images/fatcow/bomb.png
@@ -150,24 +128,16 @@ share/emacs/site-lisp/why3.el
 %%DATADIR%%/images/fatcow/time_delete.png
 %%DATADIR%%/images/fatcow/timeline.png
 %%DATADIR%%/images/fatcow/update.png
-%%DATADIR%%/images/icons.rc
 %%DATADIR%%/images/logo-why.png
-%%DATADIR%%/javascript/jquery.js
-%%DATADIR%%/javascript/jquery.jstree.js
-%%DATADIR%%/javascript/session.css
-%%DATADIR%%/javascript/session.js
-%%DATADIR%%/javascript/themes/default/d.gif
-%%DATADIR%%/javascript/themes/default/d.png
-%%DATADIR%%/javascript/themes/default/style.css
-%%DATADIR%%/javascript/themes/default/throbber.gif
 %%DATADIR%%/lang/why3.lang
 %%DATADIR%%/modules/array.mlw
-%%DATADIR%%/modules/bv.mlw
 %%DATADIR%%/modules/hashtbl.mlw
 %%DATADIR%%/modules/impset.mlw
 %%DATADIR%%/modules/io.mlw
 %%DATADIR%%/modules/mach/array.mlw
+%%DATADIR%%/modules/mach/bv.mlw
 %%DATADIR%%/modules/mach/int.mlw
+%%DATADIR%%/modules/mach/matrix.mlw
 %%DATADIR%%/modules/mach/onetime.mlw
 %%DATADIR%%/modules/mach/peano.mlw
 %%DATADIR%%/modules/matrix.mlw
@@ -183,6 +153,7 @@ share/emacs/site-lisp/why3.el
 %%DATADIR%%/theories/bag.why
 %%DATADIR%%/theories/bintree.why
 %%DATADIR%%/theories/bool.why
+%%DATADIR%%/theories/bv.why
 %%DATADIR%%/theories/floating_point.why
 %%DATADIR%%/theories/function.why
 %%DATADIR%%/theories/graph.why