|
| 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: "https://www.why3.org/" |
| 12 | +license: "LGPL-2.1-only" |
| 13 | +doc: "https://www.why3.org/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-mpfr" {!mlmpfr:installed} |
| 36 | + "--enable-mpfr" {mlmpfr:installed} |
| 37 | + "--disable-zip" {!camlzip:installed} |
| 38 | + "--enable-zip" {camlzip:installed} |
| 39 | + "--disable-hypothesis-selection" {!ocamlgraph:installed} |
| 40 | + "--enable-hypothesis-selection" {ocamlgraph:installed} |
| 41 | + "--disable-stackify" {!ocamlgraph:installed | ocaml:version < "4.12"} |
| 42 | + "--enable-stackify" {ocamlgraph:installed & ocaml:version >= "4.12"} |
| 43 | + "--disable-ide"] |
| 44 | + [make "-j%{jobs}%" "all" "byte"] |
| 45 | + [make "doc" "stdlibdoc" "apidoc"] {with-doc} |
| 46 | +] |
| 47 | + |
| 48 | +install: [ |
| 49 | + [make "install" "install-lib"] |
| 50 | + [make "DOCDIR=%{_:doc}%" "install-doc"] {with-doc} |
| 51 | +] |
| 52 | + |
| 53 | +depends: [ |
| 54 | + "conf-autoconf" {build & dev} |
| 55 | + "ocaml" {>= "4.09" & < "5.4"} |
| 56 | + "ocamlfind" {build} |
| 57 | + "menhir" {>= "20200211"} |
| 58 | + "zarith" |
| 59 | +] |
| 60 | + |
| 61 | +depopts: [ |
| 62 | + "camlzip" |
| 63 | + "ocamlgraph" |
| 64 | + "sexplib" |
| 65 | + "ppx_deriving" {build} |
| 66 | + "ppx_sexp_conv" {build} |
| 67 | + "mlmpfr" |
| 68 | +] |
| 69 | + |
| 70 | +conflicts: [ |
| 71 | + "why3-base" |
| 72 | + "ocamlgraph" {< "1.8.2"} |
| 73 | + "mlmpfr" {< "4.0.0"} |
| 74 | +] |
| 75 | + |
| 76 | +synopsis: "Why3 environment for deductive program verification" |
| 77 | + |
| 78 | +description: """ |
| 79 | +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 or C programs through an automated extraction mechanism. WhyML is also used as an intermediate language for the verification of C, Java, Rust, and Ada programs. |
| 80 | + |
| 81 | +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.""" |
| 82 | + |
| 83 | +url { |
| 84 | + src: "https://why3.gitlabpages.inria.fr/releases/why3-1.8.1.tar.gz" |
| 85 | + checksum: [ |
| 86 | + "sha256=4528fcf5b3fc64175340cef1e5ca494ec939e5221795cd925cc423e90d46156f" |
| 87 | + "md5=0a314008e7832f5cab1d4ec9f1019545" |
| 88 | + ] |
| 89 | +} |
0 commit comments