|
| 1 | +opam-version: "2.0" |
| 2 | + |
| 3 | +authors: [ |
| 4 | + "François Bobot" |
| 5 | + "Jean-Christophe Filliâtre" |
| 6 | + "Claude Marché" |
| 7 | + "Guillaume Melquiond" |
| 8 | + "Andrei Paskevich" |
| 9 | +] |
| 10 | + |
| 11 | +homepage: "http://why3.lri.fr/" |
| 12 | +license: "LGPL-2.1-only" |
| 13 | +doc: "http://why3.lri.fr/doc/" |
| 14 | +bug-reports: "https://gitlab.inria.fr/why3/why3/issues" |
| 15 | +dev-repo: "git+https://gitlab.inria.fr/why3/why3.git" |
| 16 | + |
| 17 | +tags: [ |
| 18 | + "deductive" |
| 19 | + "program verification" |
| 20 | + "formal specification" |
| 21 | + "automated theorem prover" |
| 22 | + "interactive theorem prover" |
| 23 | +] |
| 24 | + |
| 25 | +build: [ |
| 26 | + ["./autogen.sh"] {dev} # when pinning, there might be no configure file |
| 27 | + ["touch" "configure"] |
| 28 | + ["./configure" |
| 29 | + "--prefix" prefix |
| 30 | + "--disable-frama-c" |
| 31 | + "--disable-coq-libs" |
| 32 | + "--disable-js-of-ocaml" |
| 33 | + "--disable-re" |
| 34 | + "--enable-ocamlfind" |
| 35 | + "--disable-zarith" {!zarith:installed} |
| 36 | + "--enable-zarith" {zarith:installed} |
| 37 | + "--disable-mpfr" {!mlmpfr:installed} |
| 38 | + "--enable-mpfr" {mlmpfr:installed} |
| 39 | + "--disable-zip" {!camlzip:installed} |
| 40 | + "--enable-zip" {camlzip:installed} |
| 41 | + "--disable-hypothesis-selection" {!ocamlgraph:installed} |
| 42 | + "--enable-hypothesis-selection" {ocamlgraph:installed} |
| 43 | + "--disable-stackify" {!ocamlgraph:installed} |
| 44 | + "--enable-stackify" {ocamlgraph:installed} |
| 45 | + "--disable-ide"] |
| 46 | + [make "-j%{jobs}%" "all" "opt" "byte"] |
| 47 | + [make "doc" "stdlibdoc" "apidoc"] {with-doc} |
| 48 | +] |
| 49 | + |
| 50 | +install: [ |
| 51 | + [make "install" "install-lib"] |
| 52 | + [make "DOCDIR=%{_:doc}%" "install-doc"] {with-doc} |
| 53 | +] |
| 54 | + |
| 55 | +depends: [ |
| 56 | + "conf-autoconf" {build & dev} |
| 57 | + "ocaml" {>= "4.08.0"} |
| 58 | + "ocamlfind" {build} |
| 59 | + "menhir" {>= "20170418"} |
| 60 | + "num" |
| 61 | +] |
| 62 | + |
| 63 | +depopts: [ |
| 64 | + "zarith" |
| 65 | + "camlzip" |
| 66 | + "ocamlgraph" |
| 67 | + "sexplib" |
| 68 | + "ppx_deriving" {build} |
| 69 | + "ppx_sexp_conv" {build} |
| 70 | + "mlmpfr" |
| 71 | +] |
| 72 | + |
| 73 | +conflicts: [ |
| 74 | + "why3-base" |
| 75 | + "ocamlgraph" {< "1.8.2"} |
| 76 | + "mlmpfr" {< "4.0.0"} |
| 77 | + "base-effects" |
| 78 | +] |
| 79 | + |
| 80 | +synopsis: "Why3 environment for deductive program verification" |
| 81 | + |
| 82 | +description: """ |
| 83 | +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. |
| 84 | + |
| 85 | +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.""" |
| 86 | + |
| 87 | +url { |
| 88 | + src: "https://why3.gitlabpages.inria.fr/releases/why3-1.7.0.tar.gz" |
| 89 | + checksum: "md5=8e0d729aacf4980280ea251165d6867b" |
| 90 | +} |
0 commit comments