From owner-svn-ports-all@freebsd.org Sun Jun 12 13:09:24 2016 Return-Path: Delivered-To: svn-ports-all@mailman.ysv.freebsd.org Received: from mx1.freebsd.org (mx1.freebsd.org [IPv6:2001:1900:2254:206a::19:1]) by mailman.ysv.freebsd.org (Postfix) with ESMTP id 4139FAF0B78; Sun, 12 Jun 2016 13:09:24 +0000 (UTC) (envelope-from marino@FreeBSD.org) Received: from repo.freebsd.org (repo.freebsd.org [IPv6:2610:1c1:1:6068::e6a:0]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (Client did not present a certificate) by mx1.freebsd.org (Postfix) with ESMTPS id 186512FB4; Sun, 12 Jun 2016 13:09:24 +0000 (UTC) (envelope-from marino@FreeBSD.org) Received: from repo.freebsd.org ([127.0.1.37]) by repo.freebsd.org (8.15.2/8.15.2) with ESMTP id u5CD9NBJ077117; Sun, 12 Jun 2016 13:09:23 GMT (envelope-from marino@FreeBSD.org) Received: (from marino@localhost) by repo.freebsd.org (8.15.2/8.15.2/Submit) id u5CD9MFV077113; Sun, 12 Jun 2016 13:09:22 GMT (envelope-from marino@FreeBSD.org) Message-Id: <201606121309.u5CD9MFV077113@repo.freebsd.org> X-Authentication-Warning: repo.freebsd.org: marino set sender to marino@FreeBSD.org using -f From: John Marino Date: Sun, 12 Jun 2016 13:09:22 +0000 (UTC) To: ports-committers@freebsd.org, svn-ports-all@freebsd.org, svn-ports-head@freebsd.org Subject: svn commit: r416798 - in head/math/why3-spark: . files X-SVN-Group: ports-head MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit X-BeenThere: svn-ports-all@freebsd.org X-Mailman-Version: 2.1.22 Precedence: list List-Id: SVN commit messages for the ports tree List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Sun, 12 Jun 2016 13:09:24 -0000 Author: marino Date: Sun Jun 12 13:09:22 2016 New Revision: 416798 URL: https://svnweb.freebsd.org/changeset/ports/416798 Log: math/why3-spark: Upgrade version 2015 => 2016 (unbreaks) Deleted: head/math/why3-spark/files/ Modified: head/math/why3-spark/Makefile head/math/why3-spark/distinfo head/math/why3-spark/pkg-descr head/math/why3-spark/pkg-plist Modified: head/math/why3-spark/Makefile ============================================================================== --- head/math/why3-spark/Makefile Sun Jun 12 12:22:29 2016 (r416797) +++ head/math/why3-spark/Makefile Sun Jun 12 13:09:22 2016 (r416798) @@ -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 Modified: head/math/why3-spark/distinfo ============================================================================== --- head/math/why3-spark/distinfo Sun Jun 12 12:22:29 2016 (r416797) +++ head/math/why3-spark/distinfo Sun Jun 12 13:09:22 2016 (r416798) @@ -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 Modified: head/math/why3-spark/pkg-descr ============================================================================== --- head/math/why3-spark/pkg-descr Sun Jun 12 12:22:29 2016 (r416797) +++ head/math/why3-spark/pkg-descr Sun Jun 12 13:09:22 2016 (r416798) @@ -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/ Modified: head/math/why3-spark/pkg-plist ============================================================================== --- head/math/why3-spark/pkg-plist Sun Jun 12 12:22:29 2016 (r416797) +++ head/math/why3-spark/pkg-plist Sun Jun 12 13:09:22 2016 (r416798) @@ -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