Index: head/math/why3-spark/files/patch-Makefile.in =================================================================== --- head/math/why3-spark/files/patch-Makefile.in (revision 416797) +++ head/math/why3-spark/files/patch-Makefile.in (nonexistent) @@ -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 - Property changes on: head/math/why3-spark/files/patch-Makefile.in ___________________________________________________________________ Deleted: fbsd:nokeywords ## -1 +0,0 ## -yes \ No newline at end of property Deleted: svn:eol-style ## -1 +0,0 ## -native \ No newline at end of property Deleted: svn:mime-type ## -1 +0,0 ## -text/plain \ No newline at end of property Index: head/math/why3-spark/files/patch-src_tools_cpulimit.c =================================================================== --- head/math/why3-spark/files/patch-src_tools_cpulimit.c (revision 416797) +++ head/math/why3-spark/files/patch-src_tools_cpulimit.c (nonexistent) @@ -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 - #include - #include -+#include - #include - #include - Property changes on: head/math/why3-spark/files/patch-src_tools_cpulimit.c ___________________________________________________________________ Deleted: fbsd:nokeywords ## -1 +0,0 ## -yes \ No newline at end of property Deleted: svn:eol-style ## -1 +0,0 ## -native \ No newline at end of property Deleted: svn:mime-type ## -1 +0,0 ## -text/plain \ No newline at end of property Index: head/math/why3-spark/Makefile =================================================================== --- head/math/why3-spark/Makefile (revision 416797) +++ head/math/why3-spark/Makefile (revision 416798) @@ -1,50 +1,57 @@ # Created by: John Marino # $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 MAINTAINER= marino@FreeBSD.org 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 \ lablgtk2:x11-toolkits/ocaml-lablgtk2 \ 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 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 + ${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 Index: head/math/why3-spark/distinfo =================================================================== --- head/math/why3-spark/distinfo (revision 416797) +++ head/math/why3-spark/distinfo (revision 416798) @@ -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 Index: head/math/why3-spark/pkg-descr =================================================================== --- head/math/why3-spark/pkg-descr (revision 416797) +++ head/math/why3-spark/pkg-descr (revision 416798) @@ -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/ Index: head/math/why3-spark/pkg-plist =================================================================== --- head/math/why3-spark/pkg-plist (revision 416797) +++ head/math/why3-spark/pkg-plist (revision 416798) @@ -1,203 +1,174 @@ bin/gnatwhy3 bin/why3 -bin/why3-cpulimit -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/why3extract.a %%OCAML_SITELIBDIR%%/why3/why3extract.cmi %%OCAML_SITELIBDIR%%/why3/why3extract.cmx %%OCAML_SITELIBDIR%%/why3/why3extract.cmxa 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 +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 %%DATADIR%%/drivers/beagle.drv %%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 %%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-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 %%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/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 %%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/bv.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