From 0b120e989b5841e3db28687c580ac2d10a8d2795 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Thu, 11 Jan 2018 17:58:40 +0100
Subject: [PATCH] Why3 0.88.3

---
 packages/why3-base/why3-base.0.88.3/descr |  4 ++
 packages/why3-base/why3-base.0.88.3/opam  | 66 +++++++++++++++++++++++
 packages/why3-base/why3-base.0.88.3/url   |  2 +
 packages/why3/why3.0.88.3/descr           | 20 +++++++
 packages/why3/why3.0.88.3/opam            | 38 +++++++++++++
 5 files changed, 130 insertions(+)
 create mode 100644 packages/why3-base/why3-base.0.88.3/descr
 create mode 100644 packages/why3-base/why3-base.0.88.3/opam
 create mode 100644 packages/why3-base/why3-base.0.88.3/url
 create mode 100644 packages/why3/why3.0.88.3/descr
 create mode 100644 packages/why3/why3.0.88.3/opam

diff --git a/packages/why3-base/why3-base.0.88.3/descr b/packages/why3-base/why3-base.0.88.3/descr
new file mode 100644
index 00000000000..0414d9e17f1
--- /dev/null
+++ b/packages/why3-base/why3-base.0.88.3/descr
@@ -0,0 +1,4 @@
+Why3 environment for deductive program verification (base)
+
+This package is for advanced users only, normal users should use the
+full why3 package.
diff --git a/packages/why3-base/why3-base.0.88.3/opam b/packages/why3-base/why3-base.0.88.3/opam
new file mode 100644
index 00000000000..c51a8226def
--- /dev/null
+++ b/packages/why3-base/why3-base.0.88.3/opam
@@ -0,0 +1,66 @@
+opam-version: "1.2"
+maintainer: "guillaume.melquiond@inria.fr"
+authors: [
+  "François Bobot"
+  "Jean-Christophe Filliâtre"
+  "Claude Marché"
+  "Guillaume Melquiond"
+  "Andrei Paskevich"
+]
+
+homepage: "http://why3.lri.fr/"
+license: "GNU Lesser General Public License version 2.1"
+doc: "http://why3.lri.fr/doc/"
+bug-reports: "https://gitlab.inria.fr/why3/why3/issues"
+dev-repo: "https://gitlab.inria.fr/why3/why3.git"
+
+tags: [
+  "deductive"
+  "program verification"
+  "formal specification"
+  "automated theorem prover"
+  "interactive theorem prover"
+]
+available: [ ocaml-version >= "4.02.3" ]
+
+# Jessie3 (frama-c plugin) is *disabled* because it is not ready
+build: [
+  ["./configure" "--prefix" prefix "--disable-frama-c"
+                 "--disable-ide" { !conf-gtksourceview:installed }]
+  [make "-j%{jobs}%" "all" "opt" "byte"]
+]
+
+install: [make "install_no_local" "install_no_local_lib"]
+
+remove: [
+  ["rm" "%{bin}%/why3"]
+  ["rm" "-r" "%{lib}%/why3"]
+  ["rm" "-r" "%{share}%/why3"]
+]
+
+build-doc: [
+  [make "doc" "stdlibdoc" "apidoc"]
+  [make "DOCDIR=%{doc}%/why3" "install-doc"]
+]
+
+depends: [
+  "ocamlfind" {build}
+  "menhir"
+  "num"
+]
+
+depopts: [
+  "lablgtk"
+  "conf-gtksourceview"
+  "zarith"
+  "camlzip"
+  "ocamlgraph"
+  "coq"
+]
+
+conflicts: [
+  "lablgtk" {< "2.14.2"}
+  "ocamlgraph" {< "1.8.2"}
+  "coq" {< "8.4"}
+  "coq" {>= "8.8"}
+]
diff --git a/packages/why3-base/why3-base.0.88.3/url b/packages/why3-base/why3-base.0.88.3/url
new file mode 100644
index 00000000000..afa748f4838
--- /dev/null
+++ b/packages/why3-base/why3-base.0.88.3/url
@@ -0,0 +1,2 @@
+archive: "https://gforge.inria.fr/frs/download.php/file/37313/why3-0.88.3.tar.gz"
+checksum: "1ee0fd41075ba5e77a4b94ad0cc2dd43"
diff --git a/packages/why3/why3.0.88.3/descr b/packages/why3/why3.0.88.3/descr
new file mode 100644
index 00000000000..739e1800a2b
--- /dev/null
+++ b/packages/why3/why3.0.88.3/descr
@@ -0,0 +1,20 @@
+Why3 environment for deductive program verification.
+
+Why3 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.
diff --git a/packages/why3/why3.0.88.3/opam b/packages/why3/why3.0.88.3/opam
new file mode 100644
index 00000000000..7198d223412
--- /dev/null
+++ b/packages/why3/why3.0.88.3/opam
@@ -0,0 +1,38 @@
+opam-version: "1.2"
+maintainer: "guillaume.melquiond@inria.fr"
+authors: [
+  "François Bobot"
+  "Jean-Christophe Filliâtre"
+  "Claude Marché"
+  "Guillaume Melquiond"
+  "Andrei Paskevich"
+]
+
+homepage: "http://why3.lri.fr/"
+license: "GNU Lesser General Public License version 2.1"
+doc: "http://why3.lri.fr/doc/"
+bug-reports: "https://gitlab.inria.fr/why3/why3/issues"
+dev-repo: "https://gitlab.inria.fr/why3/why3.git"
+
+tags: [
+  "deductive"
+  "program verification"
+  "formal specification"
+  "automated theorem prover"
+  "interactive theorem prover"
+]
+available: [ ocaml-version >= "4.02.3" ]
+depends: [
+  "why3-base" { = "0.88.3" }
+  "lablgtk"
+  "conf-gtksourceview"
+  "zarith"
+  "camlzip"
+  "ocamlgraph"
+]
+depopts: [
+  "coq"
+]
+messages: [
+  "Coq realizations of Why3 theories are only available if Coq is installed" { !coq:installed }
+]