kpriv/freebsd-ports
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity

Add two new math ports: why3 and why3-gpl

Browse source 
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.
This commit is contained in:
John Marino 2014-06-04 19:22:33 +00:00
parent c3818dca2c
commit bf1b55a763
Notes: svn2git 2021-03-31 03:12:20 +00:00 
svn path=/head/; revision=356538
13 changed files with 599 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
math/Makefile
View file

@ -660,6 +660,8 @@
SUBDIR += vtk6
SUBDIR += wcalc
SUBDIR += wfmath
SUBDIR += why3
SUBDIR += why3-gpl
SUBDIR += wingz3
SUBDIR += wxMaxima
SUBDIR += x12arima

21
math/why3-gpl/Makefile Normal file
View file

@ -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>

2
math/why3-gpl/distinfo Normal file
View file

@ -0,0 +1,2 @@
SHA256 (why3-gpl-2014-src.tar.gz) = 0f598327b3c27f98bc7064929d990d422303155d106b1d9eb48246c039415e9e
SIZE (why3-gpl-2014-src.tar.gz) = 4568701

10
math/why3-gpl/files/patch-Makefile.in Normal file
View file

@ -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@

10
math/why3-gpl/files/patch-src_tools_cpulimit.c Normal file
View file

@ -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>

24
math/why3-gpl/pkg-descr Normal file
View file

@ -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

199
math/why3-gpl/pkg-plist Normal file
View file

@ -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%%

22
math/why3/Makefile Normal file
View file

@ -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>

73
math/why3/Makefile.common Normal file
View file

@ -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

2
math/why3/distinfo Normal file
View file

@ -0,0 +1,2 @@
SHA256 (why3-0.83.tar.gz) = cabf67e939e3422e491ef596f1a09ceaf1615642904182097cebde90e42e9ac9
SIZE (why3-0.83.tar.gz) = 5347628

10
math/why3/files/patch-src_tools_cpulimit.c Normal file
View file

@ -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>

20
math/why3/pkg-descr Normal file
View file

@ -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

204
math/why3/pkg-plist Normal file
View file

@ -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%%