-
Notifications
You must be signed in to change notification settings - Fork 1.2k
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #25103 from silene/why3-1.7.1
Why3 1.7.1
- Loading branch information
Showing
3 changed files
with
218 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,64 @@ | ||
| opam-version: "2.0" | ||
| maintainer: "guillaume.melquiond@inria.fr" | ||
| authors: [ | ||
| "François Bobot" | ||
| "Jean-Christophe Filliâtre" | ||
| "Claude Marché" | ||
| "Guillaume Melquiond" | ||
| "Andrei Paskevich" | ||
| ] | ||
|
|
||
| homepage: "https://www.why3.org/" | ||
| license: "LGPL-2.1-only" | ||
| doc: "https://www.why3.org/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" | ||
| "--enable-coq-libs"] | ||
| [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.1.tar.gz" | ||
| checksum: "md5=61397fa705f42f680d35aff29e8fd25c" | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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: "https://www.why3.org/" | ||
| license: "LGPL-2.1-only" | ||
| doc: "https://www.why3.org/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.1.tar.gz" | ||
| checksum: "md5=61397fa705f42f680d35aff29e8fd25c" | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,91 @@ | ||
| opam-version: "2.0" | ||
| maintainer: "guillaume.melquiond@inria.fr" | ||
| authors: [ | ||
| "François Bobot" | ||
| "Jean-Christophe Filliâtre" | ||
| "Claude Marché" | ||
| "Guillaume Melquiond" | ||
| "Andrei Paskevich" | ||
| ] | ||
|
|
||
| homepage: "https://www.why3.org/" | ||
| license: "LGPL-2.1-only" | ||
| doc: "https://www.why3.org/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" | ||
| "ocaml-option-bytecode-only" | ||
| ] | ||
|
|
||
| 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.1.tar.gz" | ||
| checksum: "md5=61397fa705f42f680d35aff29e8fd25c" | ||
| } |