Index: head/math/why3-gpl/Makefile =================================================================== --- head/math/why3-gpl/Makefile (revision 390669) +++ head/math/why3-gpl/Makefile (revision 390670) @@ -1,22 +1,48 @@ # Created by: John Marino # $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 -.include "${.CURDIR}/../why3/Makefile.common" +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 Index: head/math/why3-gpl/distinfo =================================================================== --- head/math/why3-gpl/distinfo (revision 390669) +++ head/math/why3-gpl/distinfo (revision 390670) @@ -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 Index: head/math/why3-gpl/files/patch-Makefile.in =================================================================== --- head/math/why3-gpl/files/patch-Makefile.in (revision 390669) +++ head/math/why3-gpl/files/patch-Makefile.in (revision 390670) @@ -1,10 +1,26 @@ ---- 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@ -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 + Index: head/math/why3-gpl/files/patch-src_tools_cpulimit.c =================================================================== --- head/math/why3-gpl/files/patch-src_tools_cpulimit.c (revision 390669) +++ head/math/why3-gpl/files/patch-src_tools_cpulimit.c (revision 390670) @@ -1,10 +1,10 @@ ---- 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 +@@ -19,6 +19,7 @@ #include + #include #include +#include #include #include Index: head/math/why3-gpl/pkg-plist =================================================================== --- head/math/why3-gpl/pkg-plist (revision 390669) +++ head/math/why3-gpl/pkg-plist (revision 390670) @@ -1,182 +1,203 @@ 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 %%DATADIR%%/drivers/coq-common.gen %%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 %%DATADIR%%/drivers/gappa.drv %%DATADIR%%/drivers/iprover.drv %%DATADIR%%/drivers/isabelle-common.gen %%DATADIR%%/drivers/isabelle-realizations.aux %%DATADIR%%/drivers/isabelle-realize.drv %%DATADIR%%/drivers/isabelle.drv %%DATADIR%%/drivers/mathematica.drv %%DATADIR%%/drivers/mathsat.drv %%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 %%DATADIR%%/drivers/tptp-tff1.drv %%DATADIR%%/drivers/tptp.gen %%DATADIR%%/drivers/vampire.drv %%DATADIR%%/drivers/verit.drv %%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 %%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%%/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 %%DATADIR%%/images/fatcow/bullet_red.png %%DATADIR%%/images/fatcow/bullet_white.png %%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 %%DATADIR%%/images/fatcow/folder.png %%DATADIR%%/images/fatcow/help.png %%DATADIR%%/images/fatcow/magic_wand_2.png %%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 %%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/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 %%DATADIR%%/modules/ref.mlw %%DATADIR%%/modules/stack.mlw %%DATADIR%%/modules/string.mlw %%DATADIR%%/provers-detection-data.conf %%DATADIR%%/theories/algebra.why %%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 %%DATADIR%%/theories/int.why %%DATADIR%%/theories/list.why %%DATADIR%%/theories/map.why %%DATADIR%%/theories/number.why %%DATADIR%%/theories/option.why %%DATADIR%%/theories/pigeon.why %%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 %%DATADIR%%/vim/why3.vim %%DATADIR%%/why3session.dtd