math/why3-gpl: upgrade version 2014 => 2015

While here, decouple this port from math/why3.  They are diverging fast.
This port is needed to build SPARK 2015 binaries which will be installed
by the lang/spark port (rather than building from source)

5 files changed, 90 insertions, 27 deletions

diff --git a/math/why3-gpl/Makefile b/math/why3-gpl/Makefile
index 6e27f7822b41..723e20ca26e8 100644
--- a/math/why3-gpl/Makefile
+++ b/math/why3-gpl/Makefile
@@ -2,21 +2,47 @@
 # $FreeBSD$
 
 PORTNAME=	why3
-PORTVERSION=	2014
-PORTREVISION=	1
+PORTVERSION=	2015
 CATEGORIES=	math
 MASTER_SITES=	http://downloads.dragonlace.net/src/ \
 		LOCAL/marino
 PKGNAMESUFFIX=	-gpl
-DISTNAME=	${PORTNAME}${PKGNAMESUFFIX}-${PORTVERSION}-src
+DISTNAME=	why3-for-spark-gpl-${PORTVERSION}-src
 
 MAINTAINER=	marino@FreeBSD.org
-COMMENT=	Component of SPARK 2014
+COMMENT=	Component of SPARK 2015
 
 LICENSE=	LGPL21 GPLv3
 LICENSE_COMB=	multi
 
-ALL_TARGET= all
+BUILD_DEPENDS=	menhir:${PORTSDIR}/devel/menhir \
+		ocaml-zip>1:${PORTSDIR}/archivers/ocaml-zip \
+		ocaml-zarith>1.2:${PORTSDIR}/math/ocaml-zarith \
+		lablgtk2:${PORTSDIR}/x11-toolkits/ocaml-lablgtk2 \
+		ocaml-sqlite3>2:${PORTSDIR}/databases/ocaml-sqlite3 \
+		ocaml-ocamlgraph>1.8:${PORTSDIR}/math/ocaml-ocamlgraph \
+		camlp5o:${PORTSDIR}/devel/ocaml-camlp5
+
+USES=		gmake
+USE_OCAML=	yes
+ALL_TARGET=	all
+GNU_CONFIGURE=	yes
+INSTALL_TARGET=	install-all
+
+MAKE_JOBS_UNSAFE=	yes
+
+CONFIGURE_ARGS=	--enable-relocation \
+		--disable-doc \
+		--disable-pvs-libs \
+		--disable-profiling \
+		--disable-coq-tactic \
+		--disable-coq-libs \
+		--disable-isabelle-libs
+
+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
 
-.include "${.CURDIR}/../why3/Makefile.common"
 .include <bsd.port.mk>
diff --git a/math/why3-gpl/distinfo b/math/why3-gpl/distinfo
index 2d7f02295e15..2a3be98e5d50 100644
--- a/math/why3-gpl/distinfo
+++ b/math/why3-gpl/distinfo
@@ -1,2 +1,2 @@
-SHA256 (why3-gpl-2014-src.tar.gz) = 0f598327b3c27f98bc7064929d990d422303155d106b1d9eb48246c039415e9e
-SIZE (why3-gpl-2014-src.tar.gz) = 4568701
+SHA256 (why3-for-spark-gpl-2015-src.tar.gz) = 90faf6001e4a9d9ccb7c913df8a2316bef004aaf9546a9a5ff6b08c28ff74ede
+SIZE (why3-for-spark-gpl-2015-src.tar.gz) = 6880072
diff --git a/math/why3-gpl/files/patch-Makefile.in b/math/why3-gpl/files/patch-Makefile.in
index 6d87243ab3a5..9c962d3cea78 100644
--- a/math/why3-gpl/files/patch-Makefile.in
+++ b/math/why3-gpl/files/patch-Makefile.in
@@ -1,6 +1,6 @@
---- Makefile.in.orig	2014-04-03 10:14:03.000000000 +0000
+--- Makefile.in.orig	2015-06-26 21:21:27 UTC
 +++ Makefile.in
-@@ -46,7 +46,6 @@ OCAMLLIB  = @OCAMLLIB@
+@@ -45,7 +45,6 @@ OCAMLLIB  = @OCAMLLIB@
  OCAMLINSTALLLIB  = $(DESTDIR)@OCAMLINSTALLLIB@
  OCAMLBEST = @OCAMLBEST@
  OCAMLVERSION = @OCAMLVERSION@
@@ -8,3 +8,19 @@
  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-gpl/files/patch-src_tools_cpulimit.c b/math/why3-gpl/files/patch-src_tools_cpulimit.c
index 5c905ece014a..f10f73f2aff3 100644
--- a/math/why3-gpl/files/patch-src_tools_cpulimit.c
+++ b/math/why3-gpl/files/patch-src_tools_cpulimit.c
@@ -1,8 +1,8 @@
---- src/tools/cpulimit.c.orig	2014-03-14 15:01:03.000000000 +0000
+--- src/tools/cpulimit.c.orig	2015-05-06 10:55:30 UTC
 +++ src/tools/cpulimit.c
-@@ -18,6 +18,7 @@
- #include <stdlib.h>
+@@ -19,6 +19,7 @@
  #include <unistd.h>
+ #include <signal.h>
  #include <errno.h>
 +#include <signal.h>
  #include <string.h>
diff --git a/math/why3-gpl/pkg-plist b/math/why3-gpl/pkg-plist
index ebfca7cbfc99..a85c8ed25d60 100644
--- a/math/why3-gpl/pkg-plist
+++ b/math/why3-gpl/pkg-plist
@@ -1,33 +1,37 @@
 bin/gnatwhy3
 bin/why3
 bin/why3-cpulimit
-bin/why3bench
-bin/why3config
-bin/why3doc
-bin/why3ide
-bin/why3replayer
-bin/why3session
+bin/why3server
 %%OCAML_SITELIBDIR%%/why3/META
 %%OCAML_SITELIBDIR%%/why3/why3.a
 %%OCAML_SITELIBDIR%%/why3/why3.cmi
 %%OCAML_SITELIBDIR%%/why3/why3.cmx
 %%OCAML_SITELIBDIR%%/why3/why3.cmxa
-%%OCAML_SITELIBDIR%%/why3/why3.o
 %%OCAML_SITELIBDIR%%/why3/why3extract.a
 %%OCAML_SITELIBDIR%%/why3/why3extract.cmi
 %%OCAML_SITELIBDIR%%/why3/why3extract.cmx
 %%OCAML_SITELIBDIR%%/why3/why3extract.cmxa
-%%OCAML_SITELIBDIR%%/why3/why3extract.o
+lib/why3/commands/why3config
+lib/why3/commands/why3doc
+lib/why3/commands/why3execute
+lib/why3/commands/why3extract
+lib/why3/commands/why3ide
+lib/why3/commands/why3prove
+lib/why3/commands/why3realize
+lib/why3/commands/why3replay
+lib/why3/commands/why3session
+lib/why3/commands/why3wc
 lib/why3/plugins/dimacs.cmxs
 lib/why3/plugins/genequlin.cmxs
 lib/why3/plugins/hypothesis_selection.cmxs
 lib/why3/plugins/tptp.cmxs
 lib/why3/why3-call-pvs
+share/emacs/site-lisp/why3.el
+%%DATADIR%%/LICENSE
 %%DATADIR%%/drivers/alt_ergo.drv
-%%DATADIR%%/drivers/alt_ergo_0.92.drv
 %%DATADIR%%/drivers/alt_ergo_0.93.drv
 %%DATADIR%%/drivers/alt_ergo_0.94.drv
-%%DATADIR%%/drivers/alt_ergo_bare.drv
+%%DATADIR%%/drivers/alt_ergo_common.drv
 %%DATADIR%%/drivers/alt_ergo_model.drv
 %%DATADIR%%/drivers/alt_ergo_smt2.drv
 %%DATADIR%%/drivers/beagle.drv
@@ -35,11 +39,13 @@ lib/why3/why3-call-pvs
 %%DATADIR%%/drivers/coq-realizations.aux
 %%DATADIR%%/drivers/coq-realize.drv
 %%DATADIR%%/drivers/coq.drv
-%%DATADIR%%/drivers/coq_8_4.drv
 %%DATADIR%%/drivers/cvc3.drv
 %%DATADIR%%/drivers/cvc3_bare.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/discrimination.gen
 %%DATADIR%%/drivers/eprover.drv
@@ -54,14 +60,19 @@ lib/why3/why3-call-pvs
 %%DATADIR%%/drivers/metis.drv
 %%DATADIR%%/drivers/metitarski.drv
 %%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/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/simplify.drv
+%%DATADIR%%/drivers/smt-libv2-bv.gen
+%%DATADIR%%/drivers/smt-libv2.drv
 %%DATADIR%%/drivers/spass.drv
 %%DATADIR%%/drivers/spass_types.drv
 %%DATADIR%%/drivers/tptp-tff0.drv
@@ -72,13 +83,13 @@ lib/why3/why3-call-pvs
 %%DATADIR%%/drivers/why3.drv
 %%DATADIR%%/drivers/why3_smt.drv
 %%DATADIR%%/drivers/why3_tptp.drv
+%%DATADIR%%/drivers/yices-smt2.drv
 %%DATADIR%%/drivers/yices.drv
 %%DATADIR%%/drivers/yices_bare.drv
 %%DATADIR%%/drivers/z3.drv
-%%DATADIR%%/drivers/z3_bare.drv
+%%DATADIR%%/drivers/z3_432.drv
 %%DATADIR%%/drivers/z3_smtv1.drv
 %%DATADIR%%/drivers/zenon.drv
-%%DATADIR%%/emacs/why3-mode.el
 %%DATADIR%%/images/boomy/accept32.png
 %%DATADIR%%/images/boomy/bug32.png
 %%DATADIR%%/images/boomy/clock32.png
@@ -94,6 +105,7 @@ lib/why3/why3-call-pvs
 %%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
@@ -114,6 +126,7 @@ lib/why3/why3-call-pvs
 %%DATADIR%%/images/fatcow/accept.png
 %%DATADIR%%/images/fatcow/bin.png
 %%DATADIR%%/images/fatcow/bomb.png
+%%DATADIR%%/images/fatcow/brick_delete.png
 %%DATADIR%%/images/fatcow/bullet_black.png
 %%DATADIR%%/images/fatcow/bullet_blue.png
 %%DATADIR%%/images/fatcow/bullet_green.png
@@ -122,6 +135,7 @@ lib/why3/why3-call-pvs
 %%DATADIR%%/images/fatcow/cancel.png
 %%DATADIR%%/images/fatcow/control_pause_blue.png
 %%DATADIR%%/images/fatcow/control_play_blue.png
+%%DATADIR%%/images/fatcow/database_delete.png
 %%DATADIR%%/images/fatcow/ddr_memory.png
 %%DATADIR%%/images/fatcow/delete.png
 %%DATADIR%%/images/fatcow/exclamation.png
@@ -131,7 +145,9 @@ lib/why3/why3-call-pvs
 %%DATADIR%%/images/fatcow/multitool.png
 %%DATADIR%%/images/fatcow/package.png
 %%DATADIR%%/images/fatcow/pencil.png
+%%DATADIR%%/images/fatcow/readme-fatcow.txt
 %%DATADIR%%/images/fatcow/script.png
+%%DATADIR%%/images/fatcow/time_delete.png
 %%DATADIR%%/images/fatcow/timeline.png
 %%DATADIR%%/images/fatcow/update.png
 %%DATADIR%%/images/icons.rc
@@ -146,11 +162,16 @@ lib/why3/why3-call-pvs
 %%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/int.mlw
+%%DATADIR%%/modules/mach/onetime.mlw
+%%DATADIR%%/modules/mach/peano.mlw
 %%DATADIR%%/modules/matrix.mlw
+%%DATADIR%%/modules/null.mlw
 %%DATADIR%%/modules/pqueue.mlw
 %%DATADIR%%/modules/queue.mlw
 %%DATADIR%%/modules/random.mlw
@@ -162,7 +183,6 @@ lib/why3/why3-call-pvs
 %%DATADIR%%/theories/bag.why
 %%DATADIR%%/theories/bintree.why
 %%DATADIR%%/theories/bool.why
-%%DATADIR%%/theories/comparison.why
 %%DATADIR%%/theories/floating_point.why
 %%DATADIR%%/theories/function.why
 %%DATADIR%%/theories/graph.why
@@ -175,6 +195,7 @@ lib/why3/why3-call-pvs
 %%DATADIR%%/theories/real.why
 %%DATADIR%%/theories/regexp.why
 %%DATADIR%%/theories/relations.why
+%%DATADIR%%/theories/seq.why
 %%DATADIR%%/theories/set.why
 %%DATADIR%%/theories/sum.why
 %%DATADIR%%/theories/tptp.why