Date: Fri, 26 Jun 2015 22:13:47 +0000 (UTC) From: John Marino <marino@FreeBSD.org> To: ports-committers@freebsd.org, svn-ports-all@freebsd.org, svn-ports-head@freebsd.org Subject: svn commit: r390670 - in head/math/why3-gpl: . files Message-ID: <201506262213.t5QMDlQI005996@svn.freebsd.org>
next in thread | raw e-mail | index | archive | help
Author: marino Date: Fri Jun 26 22:13:46 2015 New Revision: 390670 URL: https://svnweb.freebsd.org/changeset/ports/390670 Log: 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) Modified: head/math/why3-gpl/Makefile head/math/why3-gpl/distinfo head/math/why3-gpl/files/patch-Makefile.in head/math/why3-gpl/files/patch-src_tools_cpulimit.c head/math/why3-gpl/pkg-plist Modified: head/math/why3-gpl/Makefile ============================================================================== --- head/math/why3-gpl/Makefile Fri Jun 26 21:34:35 2015 (r390669) +++ head/math/why3-gpl/Makefile Fri Jun 26 22:13:46 2015 (r390670) @@ -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> Modified: head/math/why3-gpl/distinfo ============================================================================== --- head/math/why3-gpl/distinfo Fri Jun 26 21:34:35 2015 (r390669) +++ head/math/why3-gpl/distinfo Fri Jun 26 22:13:46 2015 (r390670) @@ -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 Modified: head/math/why3-gpl/files/patch-Makefile.in ============================================================================== --- head/math/why3-gpl/files/patch-Makefile.in Fri Jun 26 21:34:35 2015 (r390669) +++ head/math/why3-gpl/files/patch-Makefile.in Fri Jun 26 22:13:46 2015 (r390670) @@ -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 + Modified: head/math/why3-gpl/files/patch-src_tools_cpulimit.c ============================================================================== --- head/math/why3-gpl/files/patch-src_tools_cpulimit.c Fri Jun 26 21:34:35 2015 (r390669) +++ head/math/why3-gpl/files/patch-src_tools_cpulimit.c Fri Jun 26 22:13:46 2015 (r390670) @@ -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> Modified: head/math/why3-gpl/pkg-plist ============================================================================== --- head/math/why3-gpl/pkg-plist Fri Jun 26 21:34:35 2015 (r390669) +++ head/math/why3-gpl/pkg-plist Fri Jun 26 22:13:46 2015 (r390670) @@ -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
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?201506262213.t5QMDlQI005996>