From c7b59a92829c866e50ec00624ad6a459f0863b9c Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 24 Nov 2023 07:56:41 +0100 Subject: [PATCH 1/2] Why3 1.7.0 --- packages/why3-coq/why3-coq.1.7.0/opam | 63 +++++++++++++++++++ packages/why3-ide/why3-ide.1.7.0/opam | 63 +++++++++++++++++++ packages/why3/why3.1.7.0/opam | 90 +++++++++++++++++++++++++++ 3 files changed, 216 insertions(+) create mode 100644 packages/why3-coq/why3-coq.1.7.0/opam create mode 100644 packages/why3-ide/why3-ide.1.7.0/opam create mode 100644 packages/why3/why3.1.7.0/opam diff --git a/packages/why3-coq/why3-coq.1.7.0/opam b/packages/why3-coq/why3-coq.1.7.0/opam new file mode 100644 index 000000000000..aad4f015a991 --- /dev/null +++ b/packages/why3-coq/why3-coq.1.7.0/opam @@ -0,0 +1,63 @@ +opam-version: "2.0" +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: "LGPL-2.1-only" +doc: "http://why3.lri.fr/doc/" +bug-reports: "https://gitlab.inria.fr/why3/why3/issues" +dev-repo: "git+https://gitlab.inria.fr/why3/why3.git" + +tags: [ + "deductive" + "program verification" + "formal specification" + "automated theorem prover" + "interactive theorem prover" +] + +build: [ + ["./autogen.sh"] {dev} # when pinning, there might be no configure file + ["touch" "configure"] + ["./configure" + "--prefix" prefix + "--disable-why3-lib" + "--disable-frama-c" + "--disable-ide" + "--disable-js-of-ocaml"] + [make "-j%{jobs}%" "coq"] +] + +install: [make "install-coq"] + +depends: [ + "conf-autoconf" {build & dev} + "coq" {>= "8.11"} + "ocaml" {>= "4.08.0"} + "ocamlfind" {build} + "why3" {= version} +] + +depopts: [ + "coq-flocq" {>= "3.4"} +] + +synopsis: "Why3 environment for deductive program verification" + +description: """ +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. + +This package provides the Coq realizations of Why3 theories.""" + +url { + src: "https://why3.gitlabpages.inria.fr/releases/why3-1.7.0.tar.gz" + checksum: "md5=8e0d729aacf4980280ea251165d6867b" +} diff --git a/packages/why3-ide/why3-ide.1.7.0/opam b/packages/why3-ide/why3-ide.1.7.0/opam new file mode 100644 index 000000000000..12cad1c66498 --- /dev/null +++ b/packages/why3-ide/why3-ide.1.7.0/opam @@ -0,0 +1,63 @@ +opam-version: "2.0" +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: "LGPL-2.1-only" +doc: "http://why3.lri.fr/doc/" +bug-reports: "https://gitlab.inria.fr/why3/why3/issues" +dev-repo: "git+https://gitlab.inria.fr/why3/why3.git" + +tags: [ + "deductive" + "program verification" + "formal specification" + "automated theorem prover" + "interactive theorem prover" +] + +build: [ + ["./autogen.sh"] {dev} # when pinning, there might be no configure file + ["touch" "configure"] + ["./configure" + "--prefix" prefix + "--disable-why3-lib" + "--disable-frama-c" + "--disable-coq-libs" + "--disable-js-of-ocaml" + "--disable-re" + "--enable-ocamlfind" + "--enable-ide"] + [make "-j%{jobs}%" "ide"] +] + +install: [make "install-ide"] + +depends: [ + "conf-autoconf" {build & dev} + "ocaml" {>= "4.08.0"} + "ocamlfind" {build} + "why3" {= version} + "lablgtk3" + "lablgtk3-sourceview3" +] + +synopsis: "Why3 environment for deductive program verification" + +description: """ +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. + +This package provides an IDE for Why3.""" + +url { + src: "https://why3.gitlabpages.inria.fr/releases/why3-1.7.0.tar.gz" + checksum: "md5=8e0d729aacf4980280ea251165d6867b" +} diff --git a/packages/why3/why3.1.7.0/opam b/packages/why3/why3.1.7.0/opam new file mode 100644 index 000000000000..2bd64a2f4d1f --- /dev/null +++ b/packages/why3/why3.1.7.0/opam @@ -0,0 +1,90 @@ +opam-version: "2.0" +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: "LGPL-2.1-only" +doc: "http://why3.lri.fr/doc/" +bug-reports: "https://gitlab.inria.fr/why3/why3/issues" +dev-repo: "git+https://gitlab.inria.fr/why3/why3.git" + +tags: [ + "deductive" + "program verification" + "formal specification" + "automated theorem prover" + "interactive theorem prover" +] + +build: [ + ["./autogen.sh"] {dev} # when pinning, there might be no configure file + ["touch" "configure"] + ["./configure" + "--prefix" prefix + "--disable-frama-c" + "--disable-coq-libs" + "--disable-js-of-ocaml" + "--disable-re" + "--enable-ocamlfind" + "--disable-zarith" {!zarith:installed} + "--enable-zarith" {zarith:installed} + "--disable-mpfr" {!mlmpfr:installed} + "--enable-mpfr" {mlmpfr:installed} + "--disable-zip" {!camlzip:installed} + "--enable-zip" {camlzip:installed} + "--disable-hypothesis-selection" {!ocamlgraph:installed} + "--enable-hypothesis-selection" {ocamlgraph:installed} + "--disable-stackify" {!ocamlgraph:installed} + "--enable-stackify" {ocamlgraph:installed} + "--disable-ide"] + [make "-j%{jobs}%" "all" "opt" "byte"] + [make "doc" "stdlibdoc" "apidoc"] {with-doc} +] + +install: [ + [make "install" "install-lib"] + [make "DOCDIR=%{_:doc}%" "install-doc"] {with-doc} +] + +depends: [ + "conf-autoconf" {build & dev} + "ocaml" {>= "4.08.0"} + "ocamlfind" {build} + "menhir" {>= "20170418"} + "num" +] + +depopts: [ + "zarith" + "camlzip" + "ocamlgraph" + "sexplib" + "ppx_deriving" {build} + "ppx_sexp_conv" {build} + "mlmpfr" +] + +conflicts: [ + "why3-base" + "ocamlgraph" {< "1.8.2"} + "mlmpfr" {< "4.0.0"} + "base-effects" +] + +synopsis: "Why3 environment for deductive program verification" + +description: """ +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.""" + +url { + src: "https://why3.gitlabpages.inria.fr/releases/why3-1.7.0.tar.gz" + checksum: "md5=8e0d729aacf4980280ea251165d6867b" +} From b8b29f8b3c68f5af66f1e638bdf2e5848ce3b6f3 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 24 Nov 2023 14:48:42 +0100 Subject: [PATCH 2/2] Mark Caisar and Frama-C as incompatible with Why3 1.7 --- packages/caisar/caisar.0.2.1/opam | 2 +- packages/caisar/caisar.0.2/opam | 2 +- packages/frama-c/frama-c.27.0/opam | 2 +- packages/frama-c/frama-c.27.0~beta/opam | 2 +- packages/frama-c/frama-c.27.1/opam | 2 +- packages/frama-c/frama-c.28.0~beta/opam | 2 +- 6 files changed, 6 insertions(+), 6 deletions(-) diff --git a/packages/caisar/caisar.0.2.1/opam b/packages/caisar/caisar.0.2.1/opam index 9bf94f074c90..4656d3637971 100644 --- a/packages/caisar/caisar.0.2.1/opam +++ b/packages/caisar/caisar.0.2.1/opam @@ -25,7 +25,7 @@ depends: [ "yojson" {>= "1.7.0"} "menhirLib" {>= "20210310"} "csv" {>= "2.4"} - "why3" {>= "1.6.0"} + "why3" {>= "1.6.0" & < "1.7~"} "re" {>= "1.10.4"} "fpath" {>= "0.7.3"} "yaml" {>= "3.1.0"} diff --git a/packages/caisar/caisar.0.2/opam b/packages/caisar/caisar.0.2/opam index 2c59162148e8..400859fa2c2a 100644 --- a/packages/caisar/caisar.0.2/opam +++ b/packages/caisar/caisar.0.2/opam @@ -27,7 +27,7 @@ depends: [ "menhirLib" {>= "20210310"} "ppx_deriving_yojson" {>= "3.6.1"} "csv" {>= "2.4"} - "why3" {>= "1.6.0"} + "why3" {>= "1.6.0" & < "1.7~"} "re" {>= "1.10.4"} "fpath" {>= "0.7.3"} "yaml" {>= "3.1.0"} diff --git a/packages/frama-c/frama-c.27.0/opam b/packages/frama-c/frama-c.27.0/opam index 80e4244e228c..fd5bbd867c3c 100644 --- a/packages/frama-c/frama-c.27.0/opam +++ b/packages/frama-c/frama-c.27.0/opam @@ -128,7 +128,7 @@ depends: [ "ocamlgraph" { >= "1.8.8" } "ocamlgraph" { with-test & < "2.1.0" } "odoc" { with-doc } - "why3" { >= "1.6.0" } + "why3" { >= "1.6.0" & < "1.7~" } "yaml" { >= "3.0.0" } "yojson" {>= "1.6.0" & (>= "2.0.1" | !with-test)} "zarith" { >= "1.5" } diff --git a/packages/frama-c/frama-c.27.0~beta/opam b/packages/frama-c/frama-c.27.0~beta/opam index 271e0efd7b97..8b49f904d61d 100644 --- a/packages/frama-c/frama-c.27.0~beta/opam +++ b/packages/frama-c/frama-c.27.0~beta/opam @@ -123,7 +123,7 @@ depends: [ "ocamlfind" # needed beyond build stage, used by -load-module "ocamlgraph" { >= "1.8.8" } "ocamlgraph" { with-test & < "2.1.0" } - "why3" { >= "1.6.0" } + "why3" { >= "1.6.0" & < "1.7~" } "yaml" { >= "3.0.0" } "yojson" {>= "1.6.0" & (>= "2.0.1" | !with-test)} "zarith" { >= "1.5" } diff --git a/packages/frama-c/frama-c.27.1/opam b/packages/frama-c/frama-c.27.1/opam index 2374035d1575..d91bf86d6ecd 100644 --- a/packages/frama-c/frama-c.27.1/opam +++ b/packages/frama-c/frama-c.27.1/opam @@ -127,7 +127,7 @@ depends: [ "ocamlgraph" { >= "1.8.8" } "ocamlgraph" { with-test & < "2.1.0" } "odoc" { with-doc } - "why3" { >= "1.6.0" } + "why3" { >= "1.6.0" & < "1.7~" } "yaml" { >= "3.0.0" } "yojson" {>= "1.6.0" & (>= "2.0.1" | !with-test)} "zarith" { >= "1.5" } diff --git a/packages/frama-c/frama-c.28.0~beta/opam b/packages/frama-c/frama-c.28.0~beta/opam index 233088afd13c..19b24f7012bc 100644 --- a/packages/frama-c/frama-c.28.0~beta/opam +++ b/packages/frama-c/frama-c.28.0~beta/opam @@ -132,7 +132,7 @@ depends: [ "ocamlgraph" { with-test & >= "2.1.0" } "odoc" { with-doc } "unionFind" { >= "20220107" } - "why3" { >= "1.6.0" } + "why3" { >= "1.6.0" & < "1.7~" } "yaml" { >= "3.0.0" } "yojson" {>= "1.6.0" & (>= "2.0.1" | !with-test)} "zarith" { >= "1.5" }