Merge pull request ocaml#11215 from silene/master

Why3 0.88.3

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.

packages/why3-base/why3-base.0.88.3/opam

@@ -0,0 +1,66 @@
+opam-version: "1.2"
+maintainer: "[email protected]"
+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"}
+]

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"

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.

packages/why3/why3.0.88.3/opam

@@ -0,0 +1,38 @@
+opam-version: "1.2"
+maintainer: "[email protected]"
+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 }
+]