1 files changed, 20 insertions, 0 deletions
diff --git a/devel/why3/DETAILS b/devel/why3/DETAILS
new file mode 100755
index 0000000000..9eae05e0f5
--- /dev/null
+++ b/devel/why3/DETAILS
@@ -0,0 +1,20 @@
+           SPELL=why3
+         VERSION=0.81
+          SOURCE="${SPELL}-${VERSION}.tar.gz"
+   SOURCE_URL[0]=http://why3.lri.fr/download/${SOURCE}
+     SOURCE_HASH=sha512:1ad2b1019a7e7cf020961c0836b158682120acf058d9df28331fdf73d21abc1af34472c8afb171bb8dd3babdeef86289927cf98fc92341a6eac11f4c4ccbfe80
+SOURCE_DIRECTORY="${BUILD_DIRECTORY}/${SPELL}-${VERSION}"
+        WEB_SITE="http://why3.lri.fr"
+      LICENSE[0]=GPL
+         ENTERED=20120209
+           SHORT="a rich library of proof task transformations"
+cat << EOF
+Why3 is the next generation of the Why software verification platform. Why3
+clearly separates the purely logical specification part from generation of
+verification conditions for programs. It features a rich library of proof
+task transformations that can be chained to produce a suitable input for a
+large set of theorem provers, including SMT solvers, TPTP provers, as well
+as interactive proof assistants.
+
+Supported provers: Alt-Ergo, Z3, CVC3, Yices 1, Simplify, Gappa, Coq.
+EOF