13 files changed, 599 insertions, 0 deletions

diff --git a/math/Makefile b/math/Makefile
index fc023f3f20af..4f485c2517d9 100644
--- a/math/Makefile
+++ b/math/Makefile
@@ -660,6 +660,8 @@
     SUBDIR += vtk6
     SUBDIR += wcalc
     SUBDIR += wfmath
+    SUBDIR += why3
+    SUBDIR += why3-gpl
     SUBDIR += wingz3
     SUBDIR += wxMaxima
     SUBDIR += x12arima
diff --git a/math/why3-gpl/Makefile b/math/why3-gpl/Makefile
new file mode 100644
index 000000000000..fed0023d6833
--- /dev/null
+++ b/math/why3-gpl/Makefile
@@ -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>
diff --git a/math/why3-gpl/distinfo b/math/why3-gpl/distinfo
new file mode 100644
index 000000000000..2d7f02295e15
--- /dev/null
+++ b/math/why3-gpl/distinfo
@@ -0,0 +1,2 @@
+SHA256 (why3-gpl-2014-src.tar.gz) = 0f598327b3c27f98bc7064929d990d422303155d106b1d9eb48246c039415e9e
+SIZE (why3-gpl-2014-src.tar.gz) = 4568701
diff --git a/math/why3-gpl/files/patch-Makefile.in b/math/why3-gpl/files/patch-Makefile.in
new file mode 100644
index 000000000000..6d87243ab3a5
--- /dev/null
+++ b/math/why3-gpl/files/patch-Makefile.in
@@ -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@
diff --git a/math/why3-gpl/files/patch-src_tools_cpulimit.c b/math/why3-gpl/files/patch-src_tools_cpulimit.c
new file mode 100644
index 000000000000..5c905ece014a
--- /dev/null
+++ b/math/why3-gpl/files/patch-src_tools_cpulimit.c
@@ -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>
+ 
diff --git a/math/why3-gpl/pkg-descr b/math/why3-gpl/pkg-descr
new file mode 100644
index 000000000000..4ab076ae7288
--- /dev/null
+++ b/math/why3-gpl/pkg-descr
@@ -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
diff --git a/math/why3-gpl/pkg-plist b/math/why3-gpl/pkg-plist
new file mode 100644
index 000000000000..0a6644c4773b
--- /dev/null
+++ b/math/why3-gpl/pkg-plist
@@ -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%%
diff --git a/math/why3/Makefile b/math/why3/Makefile
new file mode 100644
index 000000000000..367a8d6ce23e
--- /dev/null
+++ b/math/why3/Makefile
@@ -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>
diff --git a/math/why3/Makefile.common b/math/why3/Makefile.common
new file mode 100644
index 000000000000..2cb742ddc043
--- /dev/null
+++ b/math/why3/Makefile.common
@@ -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
diff --git a/math/why3/distinfo b/math/why3/distinfo
new file mode 100644
index 000000000000..2c961b8aba61
--- /dev/null
+++ b/math/why3/distinfo
@@ -0,0 +1,2 @@
+SHA256 (why3-0.83.tar.gz) = cabf67e939e3422e491ef596f1a09ceaf1615642904182097cebde90e42e9ac9
+SIZE (why3-0.83.tar.gz) = 5347628
diff --git a/math/why3/files/patch-src_tools_cpulimit.c b/math/why3/files/patch-src_tools_cpulimit.c
new file mode 100644
index 000000000000..5c905ece014a
--- /dev/null
+++ b/math/why3/files/patch-src_tools_cpulimit.c
@@ -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>
+ 
diff --git a/math/why3/pkg-descr b/math/why3/pkg-descr
new file mode 100644
index 000000000000..ed0b7f1fea9c
--- /dev/null
+++ b/math/why3/pkg-descr
@@ -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
diff --git a/math/why3/pkg-plist b/math/why3/pkg-plist
new file mode 100644
index 000000000000..f59dd690d4a1
--- /dev/null
+++ b/math/why3/pkg-plist
@@ -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%%