Skip site navigation (1)Skip section navigation (2)
Date:      Wed, 4 Jun 2014 19:22:34 +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: r356538 - in head/math: . why3 why3-gpl why3-gpl/files why3/files
Message-ID:  <201406041922.s54JMYLi070630@svn.freebsd.org>

next in thread | raw e-mail | index | archive | help
Author: marino
Date: Wed Jun  4 19:22:33 2014
New Revision: 356538
URL: http://svnweb.freebsd.org/changeset/ports/356538
QAT: https://qat.redports.org/buildarchive/r356538/

Log:
  Add two new math ports: why3 and why3-gpl
  
  The primary motivation for adding why3 is to support the upcoming SPARK
  2014 port.  However, SPARK 2014 requires a custom version.  In time the
  customizations should make it upstream, but currently the stock version
  cannot be used to build SPARK.  They are also licensed differently (LGPL2
  for stock, GPLv3 for SPARK version).
  
  Rather than force people that find why3 useful on their own to accept a
  custom version, both are offered although they currently conflict.
  
  Why3 has optional dependencies on coq, isabelle, and frama-c, and all
  three have issus:
    * coq rebuilds its libraries in $LOCALBASE, could be issue with coq
    * isabella currently has a broken dependency (sjsml) and only for i386
      when it's not.  Updating to 2013-2 version failed, as did trying to
      build it with polyml instead of sjsml
    * frama-c is fine, but the plugin code in why3 is still experimental
      and upstream recommends that it not be used.
  
       ==============================================================
  
  Why3 is a platform for deductive program verification. It provides a rich
  language for specification and programming, called WhyML, and relies on
  external theorem provers, both automated and interactive, to discharge
  verification conditions. Why3 comes with a standard library of logical
  theories (integer and real arithmetic, Boolean operations, sets and maps,
  etc.) and basic programming data structures (arrays, queues, hash tables,
  etc.). A user can write WhyML programs directly and get correct-by-
  construction OCaml programs through an automated extraction mechanism.
  WhyML is also used as an intermediate language for the verification of C,
  Java, or Ada programs.
  
  Why3 is a complete reimplementation of the former Why platform. Among the
  new features are: numerous extensions to the input language, a new
  architecture for calling external provers, and a well-designed API,
  allowing to use Why3 as a software library. An important emphasis is put
  on modularity and genericity, giving the end user a possibility to easily
  reuse Why3 formalizations or to add support for a new external prover if
  wanted.

Added:
  head/math/why3/
  head/math/why3-gpl/
  head/math/why3-gpl/Makefile   (contents, props changed)
  head/math/why3-gpl/distinfo   (contents, props changed)
  head/math/why3-gpl/files/
  head/math/why3-gpl/files/patch-Makefile.in   (contents, props changed)
  head/math/why3-gpl/files/patch-src_tools_cpulimit.c   (contents, props changed)
  head/math/why3-gpl/pkg-descr   (contents, props changed)
  head/math/why3-gpl/pkg-plist   (contents, props changed)
  head/math/why3/Makefile   (contents, props changed)
  head/math/why3/Makefile.common   (contents, props changed)
  head/math/why3/distinfo   (contents, props changed)
  head/math/why3/files/
  head/math/why3/files/patch-src_tools_cpulimit.c   (contents, props changed)
  head/math/why3/pkg-descr   (contents, props changed)
  head/math/why3/pkg-plist   (contents, props changed)
Modified:
  head/math/Makefile

Modified: head/math/Makefile
==============================================================================
--- head/math/Makefile	Wed Jun  4 19:19:51 2014	(r356537)
+++ head/math/Makefile	Wed Jun  4 19:22:33 2014	(r356538)
@@ -660,6 +660,8 @@
     SUBDIR += vtk6
     SUBDIR += wcalc
     SUBDIR += wfmath
+    SUBDIR += why3
+    SUBDIR += why3-gpl
     SUBDIR += wingz3
     SUBDIR += wxMaxima
     SUBDIR += x12arima

Added: head/math/why3-gpl/Makefile
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ head/math/why3-gpl/Makefile	Wed Jun  4 19:22:33 2014	(r356538)
@@ -0,0 +1,21 @@
+# Created by: John Marino <marino@FreeBSD.org>
+# $FreeBSD$
+
+PORTNAME=	why3
+PORTVERSION=	2014
+CATEGORIES=	math
+MASTER_SITES=	http://downloads.dragonlace.net/src/ \
+		LOCAL/marino
+PKGNAMESUFFIX=	-gpl
+DISTNAME=	${PORTNAME}${PKGNAMESUFFIX}-${PORTVERSION}-src
+
+MAINTAINER=	marino@FreeBSD.org
+COMMENT=	Deductive program verification platform with SPARK support
+
+LICENSE=	LGPL21 GPLv3
+LICENSE_COMB=	multi
+
+ALL_TARGET= all
+
+.include "${.CURDIR}/../why3/Makefile.common"
+.include <bsd.port.mk>

Added: head/math/why3-gpl/distinfo
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ head/math/why3-gpl/distinfo	Wed Jun  4 19:22:33 2014	(r356538)
@@ -0,0 +1,2 @@
+SHA256 (why3-gpl-2014-src.tar.gz) = 0f598327b3c27f98bc7064929d990d422303155d106b1d9eb48246c039415e9e
+SIZE (why3-gpl-2014-src.tar.gz) = 4568701

Added: head/math/why3-gpl/files/patch-Makefile.in
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ head/math/why3-gpl/files/patch-Makefile.in	Wed Jun  4 19:22:33 2014	(r356538)
@@ -0,0 +1,10 @@
+--- Makefile.in.orig	2014-04-03 10:14:03.000000000 +0000
++++ Makefile.in
+@@ -46,7 +46,6 @@ OCAMLLIB  = @OCAMLLIB@
+ OCAMLINSTALLLIB  = $(DESTDIR)@OCAMLINSTALLLIB@
+ OCAMLBEST = @OCAMLBEST@
+ OCAMLVERSION = @OCAMLVERSION@
+-CC        = gcc
+ COQC      = @COQC@
+ COQDEP    = @COQDEP@
+ CAMLP5O   = @CAMLP5O@

Added: head/math/why3-gpl/files/patch-src_tools_cpulimit.c
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ head/math/why3-gpl/files/patch-src_tools_cpulimit.c	Wed Jun  4 19:22:33 2014	(r356538)
@@ -0,0 +1,10 @@
+--- src/tools/cpulimit.c.orig	2014-03-14 15:01:03.000000000 +0000
++++ src/tools/cpulimit.c
+@@ -18,6 +18,7 @@
+ #include <stdlib.h>
+ #include <unistd.h>
+ #include <errno.h>
++#include <signal.h>
+ #include <string.h>
+ #include <sys/wait.h>
+ 

Added: head/math/why3-gpl/pkg-descr
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ head/math/why3-gpl/pkg-descr	Wed Jun  4 19:22:33 2014	(r356538)
@@ -0,0 +1,24 @@
+Why3 is a platform for deductive program verification. It provides a rich
+language for specification and programming, called WhyML, and relies on
+external theorem provers, both automated and interactive, to discharge
+verification conditions. Why3 comes with a standard library of logical
+theories (integer and real arithmetic, Boolean operations, sets and maps,
+etc.) and basic programming data structures (arrays, queues, hash tables,
+etc.). A user can write WhyML programs directly and get correct-by-
+construction OCaml programs through an automated extraction mechanism.
+WhyML is also used as an intermediate language for the verification of C,
+Java, or Ada programs.
+
+Why3 is a complete reimplementation of the former Why platform. Among the
+new features are: numerous extensions to the input language, a new
+architecture for calling external provers, and a well-designed API,
+allowing to use Why3 as a software library. An important emphasis is put
+on modularity and genericity, giving the end user a possibility to easily
+reuse Why3 formalizations or to add support for a new external prover if
+wanted.
+
+This GPL version version of Why3 has been released by Adacore with an
+additional binary for SPARK 2014 support and some patches which have not
+yet been pushed upstream.
+
+WWW: https://forge.open-do.org/projects/spark2014

Added: head/math/why3-gpl/pkg-plist
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ head/math/why3-gpl/pkg-plist	Wed Jun  4 19:22:33 2014	(r356538)
@@ -0,0 +1,199 @@
+bin/gnatwhy3
+bin/why3
+bin/why3-cpulimit
+bin/why3bench
+bin/why3config
+bin/why3doc
+bin/why3ide
+bin/why3replayer
+bin/why3session
+%%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/plugins/dimacs.cmxs
+lib/why3/plugins/genequlin.cmxs
+lib/why3/plugins/hypothesis_selection.cmxs
+lib/why3/plugins/tptp.cmxs
+lib/why3/why3-call-pvs
+%%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_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_bare.drv
+%%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/ocaml32.drv
+%%DATADIR%%/drivers/ocaml64.drv
+%%DATADIR%%/drivers/princess.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/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.drv
+%%DATADIR%%/drivers/yices_bare.drv
+%%DATADIR%%/drivers/z3.drv
+%%DATADIR%%/drivers/z3_bare.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/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/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/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/script.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/hashtbl.mlw
+%%DATADIR%%/modules/impset.mlw
+%%DATADIR%%/modules/mach/array.mlw
+%%DATADIR%%/modules/mach/int.mlw
+%%DATADIR%%/modules/matrix.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/set.why
+%%DATADIR%%/theories/sum.why
+%%DATADIR%%/theories/tptp.why
+%%DATADIR%%/vim/why3.vim
+%%DATADIR%%/why3session.dtd
+@dirrm %%OCAML_SITELIBDIR%%/why3
+@dirrm lib/why3/plugins
+@dirrm lib/why3
+@dirrm %%DATADIR%%/drivers
+@dirrm %%DATADIR%%/emacs
+@dirrm %%DATADIR%%/images/boomy
+@dirrm %%DATADIR%%/images/fatcow
+@dirrm %%DATADIR%%/images
+@dirrm %%DATADIR%%/javascript/themes/default
+@dirrm %%DATADIR%%/javascript/themes
+@dirrm %%DATADIR%%/javascript
+@dirrm %%DATADIR%%/lang
+@dirrm %%DATADIR%%/modules/mach
+@dirrm %%DATADIR%%/modules
+@dirrm %%DATADIR%%/theories
+@dirrm %%DATADIR%%/vim
+@dirrm %%DATADIR%%

Added: head/math/why3/Makefile
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ head/math/why3/Makefile	Wed Jun  4 19:22:33 2014	(r356538)
@@ -0,0 +1,22 @@
+# Created by: John Marino <marino@FreeBSD.org>
+# $FreeBSD$
+
+PORTNAME=	why3
+PORTVERSION=	0.83
+CATEGORIES=	math
+MASTER_SITES=	http://gforge.inria.fr/frs/download.php/33490/ \
+		http://pkgs.fedoraproject.org/repo/pkgs/why3/${FEDORA}/
+
+MAINTAINER=	marino@FreeBSD.org
+COMMENT=	Deductive program verification platform
+
+LICENSE=	LGPL21
+
+CONFLICT_INSTALL= why3-gpl-*
+
+FEDORA=		${DISTNAME}${EXTRACT_SUFX}/35f99e5f64939e50ea57f641ba2073ec
+ALL_TARGET=	all byte
+HAS_MANUAL=	yes
+
+.include "${.CURDIR}/Makefile.common"
+.include <bsd.port.mk>

Added: head/math/why3/Makefile.common
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ head/math/why3/Makefile.common	Wed Jun  4 19:22:33 2014	(r356538)
@@ -0,0 +1,73 @@
+# Created by: John Marino <marino@FreeBSD.org>
+# $FreeBSD$
+
+BUILD_DEPENDS=	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
+
+GNU_CONFIGURE=	yes
+INSTALL_TARGET=	install-all
+
+USES=			gmake
+USE_OCAML=		yes
+MAKE_JOBS_UNSAFE=	yes
+
+# The FRAMA_C plugin is experimental, it actually doesn't even build
+# with ocaml 4.01.  Leave the option commented out for future use.
+# There is something wrong with coq, it rebuilds itself in /usr/local.
+# Leave it for now with a TO-DO to fix coq
+# Isabelle is currently i386-only due to issues with polyml and default
+# reliance on i386-only sml-nj (also currently broke).  Disable for now.
+
+CONFIGURE_ARGS=	--enable-relocation \
+		--disable-doc \
+		--disable-pvs-libs \
+		--disable-profiling \
+		--disable-coq-tactic \
+		--disable-coq-libs \
+		--disable-isabelle-libs
+
+.if defined(HAS_MANUAL)
+PORTDOCS=	manual.pdf
+OPTIONS_DEFINE=	DOCS #ISABELLE COQ FRAMA_C
+.endif
+
+COQ_CONFIGURE_ENABLE=		coq-tactic coq-libs
+COQ_DESC=			Build coq realizations and tactics
+COQ_BUILD_DEPENDS=		coqc:${PORTSDIR}/math/coq
+COQ_RUN_DEPENDS=		coqc:${PORTSDIR}/math/coq
+FRAMA_C_CONFIGURE_ENABLE=	frama_c
+FRAMA_C_DESC=			Build Frama-C plugin
+FRAMA_C_BUILD_DEPENDS=		frama-c:${PORTSDIR}/devel/frama-c
+FRAMA_C_RUN_DEPENDS=		frama-c:${PORTSDIR}/devel/frama-c
+ISABELLE_CONFIGURE_ENABLE=	isabelle-libs
+ISABELLE_DESC=			Enable Isabelle realizations
+ISABELLE_BUILD_DEPENDS=		isabelle:${PORTSDIR}/math/isabelle
+ISABELLE_RUN_DEPENDS=		isabelle:${PORTSDIR}/math/isabelle
+
+# The pdf is pre-built, but the makefile wants to build it again in order
+# to generate manual.bbl which is used to build the html documention.
+# Regenerating pdf fails, and the dependencies are heavy.  Disable this
+# all for now and just manually install the pdf.  The "doc" target was
+# also removed from ALL_TARGET
+#
+#DOCS_CONFIGURE_ENABLE=		doc
+#DOCS_BUILD_DEPENDS=		rubber:${PORTSDIR}/textproc/rubber \
+#				hevea:${PORTSDIR}/textproc/hevea
+
+.include <bsd.port.options.mk>
+
+post-patch:
+	@${REINPLACE_CMD} -e 's|/bin/bash|/bin/sh|g' \
+		${WRKSRC}/src/util/sysutil.ml \
+		${WRKSRC}/src/jessie/Makefile.in
+
+post-install:
+.if ${PORT_OPTIONS:MDOCS}
+.  if defined(HAS_MANUAL)
+	${MKDIR} ${STAGEDIR}${DOCSDIR}
+	${INSTALL_DATA} ${WRKSRC}/doc/manual.pdf ${STAGEDIR}${DOCSDIR}
+.  endif
+.endif

Added: head/math/why3/distinfo
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ head/math/why3/distinfo	Wed Jun  4 19:22:33 2014	(r356538)
@@ -0,0 +1,2 @@
+SHA256 (why3-0.83.tar.gz) = cabf67e939e3422e491ef596f1a09ceaf1615642904182097cebde90e42e9ac9
+SIZE (why3-0.83.tar.gz) = 5347628

Added: head/math/why3/files/patch-src_tools_cpulimit.c
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ head/math/why3/files/patch-src_tools_cpulimit.c	Wed Jun  4 19:22:33 2014	(r356538)
@@ -0,0 +1,10 @@
+--- src/tools/cpulimit.c.orig	2014-03-14 15:01:03.000000000 +0000
++++ src/tools/cpulimit.c
+@@ -18,6 +18,7 @@
+ #include <stdlib.h>
+ #include <unistd.h>
+ #include <errno.h>
++#include <signal.h>
+ #include <string.h>
+ #include <sys/wait.h>
+ 

Added: head/math/why3/pkg-descr
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ head/math/why3/pkg-descr	Wed Jun  4 19:22:33 2014	(r356538)
@@ -0,0 +1,20 @@
+Why3 is a platform for deductive program verification. It provides a rich
+language for specification and programming, called WhyML, and relies on
+external theorem provers, both automated and interactive, to discharge
+verification conditions. Why3 comes with a standard library of logical
+theories (integer and real arithmetic, Boolean operations, sets and maps,
+etc.) and basic programming data structures (arrays, queues, hash tables,
+etc.). A user can write WhyML programs directly and get correct-by-
+construction OCaml programs through an automated extraction mechanism.
+WhyML is also used as an intermediate language for the verification of C,
+Java, or Ada programs.
+
+Why3 is a complete reimplementation of the former Why platform. Among the
+new features are: numerous extensions to the input language, a new
+architecture for calling external provers, and a well-designed API,
+allowing to use Why3 as a software library. An important emphasis is put
+on modularity and genericity, giving the end user a possibility to easily
+reuse Why3 formalizations or to add support for a new external prover if
+wanted.
+
+WWW: http://why3.lri.fr

Added: head/math/why3/pkg-plist
==============================================================================
--- /dev/null	00:00:00 1970	(empty, because file is newly added)
+++ head/math/why3/pkg-plist	Wed Jun  4 19:22:33 2014	(r356538)
@@ -0,0 +1,204 @@
+bin/why3
+bin/why3bench
+bin/why3config
+bin/why3doc
+bin/why3ide
+bin/why3replayer
+bin/why3session
+%%OCAML_SITELIBDIR%%/why3/META
+%%OCAML_SITELIBDIR%%/why3/why3.a
+%%OCAML_SITELIBDIR%%/why3/why3.cma
+%%OCAML_SITELIBDIR%%/why3/why3.cmi
+%%OCAML_SITELIBDIR%%/why3/why3.cmo
+%%OCAML_SITELIBDIR%%/why3/why3.cmx
+%%OCAML_SITELIBDIR%%/why3/why3.cmxa
+%%OCAML_SITELIBDIR%%/why3/why3.o
+%%OCAML_SITELIBDIR%%/why3/why3extract.a
+%%OCAML_SITELIBDIR%%/why3/why3extract.cma
+%%OCAML_SITELIBDIR%%/why3/why3extract.cmi
+%%OCAML_SITELIBDIR%%/why3/why3extract.cmo
+%%OCAML_SITELIBDIR%%/why3/why3extract.cmx
+%%OCAML_SITELIBDIR%%/why3/why3extract.cmxa
+%%OCAML_SITELIBDIR%%/why3/why3extract.o
+lib/why3/plugins/dimacs.cmo
+lib/why3/plugins/dimacs.cmxs
+lib/why3/plugins/genequlin.cmo
+lib/why3/plugins/genequlin.cmxs
+lib/why3/plugins/hypothesis_selection.cmo
+lib/why3/plugins/hypothesis_selection.cmxs
+lib/why3/plugins/tptp.cmo
+lib/why3/plugins/tptp.cmxs
+lib/why3/why3-call-pvs
+lib/why3/why3-cpulimit
+%%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_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/cvc3.drv
+%%DATADIR%%/drivers/cvc3_bare.drv
+%%DATADIR%%/drivers/cvc4.drv
+%%DATADIR%%/drivers/cvc4_bare.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/ocaml32.drv
+%%DATADIR%%/drivers/ocaml64.drv
+%%DATADIR%%/drivers/princess.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/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.drv
+%%DATADIR%%/drivers/yices_bare.drv
+%%DATADIR%%/drivers/z3.drv
+%%DATADIR%%/drivers/z3_bare.drv
+%%DATADIR%%/drivers/z3_smtv1.drv
+%%DATADIR%%/drivers/zenon.drv
+%%DATADIR%%/emacs/why3.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/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/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/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/script.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/hashtbl.mlw
+%%DATADIR%%/modules/impset.mlw
+%%DATADIR%%/modules/mach/array.mlw
+%%DATADIR%%/modules/mach/int.mlw
+%%DATADIR%%/modules/matrix.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/set.why
+%%DATADIR%%/theories/sum.why
+%%DATADIR%%/theories/tptp.why
+%%DATADIR%%/vim/why3.vim
+%%DATADIR%%/why3session.dtd
+@dirrm %%OCAML_SITELIBDIR%%/why3
+@dirrm lib/why3/plugins
+@dirrm lib/why3
+@dirrm %%DATADIR%%/drivers
+@dirrm %%DATADIR%%/emacs
+@dirrm %%DATADIR%%/images/boomy
+@dirrm %%DATADIR%%/images/fatcow
+@dirrm %%DATADIR%%/images
+@dirrm %%DATADIR%%/javascript/themes/default
+@dirrm %%DATADIR%%/javascript/themes
+@dirrm %%DATADIR%%/javascript
+@dirrm %%DATADIR%%/lang
+@dirrm %%DATADIR%%/modules/mach
+@dirrm %%DATADIR%%/modules
+@dirrm %%DATADIR%%/theories
+@dirrm %%DATADIR%%/vim
+@dirrm %%DATADIR%%



Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?201406041922.s54JMYLi070630>