Summary
Why3 is a platform for deductive program verification. It 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.
Versions
v1.7.2 :: 0/1.7.2 :: gentoo
- Modified
- License
- LGPL-2
- Keywords
- ~amd64
- USE flags
- coq doc emacs gtk ocamlopt re sexp stackify zarith zip
v1.6.0 :: 0/1.6.0 :: gentoo
- Modified
- License
- LGPL-2
- Keywords
- ~amd64
- USE flags
- coq doc emacs gtk ocamlopt re sexp stackify zarith zip
USE flags
General
- coq
- Add sci-mathematics/coq support
- doc
- Add extra documentation (API, Javadoc, etc). It is recommended to enable per package instead of globally
- emacs
- Add support for GNU Emacs
- gtk
- Build the IDE x11-libs/gtk+
- ocamlopt
- Enable ocamlopt support (ocaml native code compiler) -- Produces faster programs (Warning: you have to disable/enable it at a global scale)
- re
- Use Re (dev-ml/re) instead of Str for regular expressions
- sexp
- Add support for outputting S-expressions with dev-ml/ppx_sexp_conv
- stackify
- Enable structure reconstruction algorithm for MLCFG
- zarith
- Use Zarith (dev-ml/zarith) instead of Nums (dev-ml/num) for computations
- zip
- Enable compression of session files
Dependencies
app-editors / emacs : The extensible, customizable, self-documenting real-time display editor
dev-lang / ocaml : Programming language supporting functional, imperative & object-oriented styles
dev-ml / camlzip : Compressed file access ML library (ZIP, GZIP and JAR)
dev-ml / findlib : OCaml tool to find/use non-standard packages
dev-ml / lablgtk : OCaml bindings to GTK-3
dev-ml / menhir : LR(1) parser generator for the OCaml language
dev-ml / num : Library for arbitrary-precision integer and rational arithmetic
dev-ml / ocamlgraph : O'Caml Graph library
dev-ml / ppx_deriving : Type-driven code generation for OCaml
dev-ml / ppx_sexp_conv : Support Library for type-driven code generators
dev-ml / re : Regular expression library for OCaml
dev-ml / sexplib : Library for automated conversion of OCaml-values to and from S-expressions
dev-ml / zarith : Arithmetic and logic operations over arbitrary-precision integers
sci-mathematics / coq : Proof assistant written in O'Caml
sci-mathematics / why3-for-spark : Platform for deductive program verification
Runtime Dependencies
app-editors / emacs : The extensible, customizable, self-documenting real-time display editor
dev-lang / ocaml : Programming language supporting functional, imperative & object-oriented styles
dev-ml / camlzip : Compressed file access ML library (ZIP, GZIP and JAR)
dev-ml / lablgtk : OCaml bindings to GTK-3
dev-ml / menhir : LR(1) parser generator for the OCaml language
dev-ml / num : Library for arbitrary-precision integer and rational arithmetic
dev-ml / ocamlgraph : O'Caml Graph library
dev-ml / ppx_deriving : Type-driven code generation for OCaml
dev-ml / ppx_sexp_conv : Support Library for type-driven code generators
dev-ml / re : Regular expression library for OCaml
dev-ml / sexplib : Library for automated conversion of OCaml-values to and from S-expressions
dev-ml / zarith : Arithmetic and logic operations over arbitrary-precision integers
sci-mathematics / coq : Proof assistant written in O'Caml
sci-mathematics / why3-for-spark : Platform for deductive program verification
Depending packages
sci-mathematics / easycrypt : Computer-Aided Cryptographic Proofs
Bugs
- 906225
- sci-mathematics/why3-1.6.0 - Error: Cannot load ppx_sexp_conv: this object file uses unsafe features
- 937720
- sci-mathematics/why3-1.6.0 - [ncurses-6.5] [icu-75.1] [gcc-15] make inconsistent assumptions over interface Nat
- 946556
- sci-mathematics/why3-1.7.2 - [texlive] [meson] Error: Cannot find a physical path bound to logical path Flocq.Version.
Change logs
- Repository mirror & CI · gentoo
Merge updates from master - Sam James · gentoo
sci-mathematics/why3: update HOMEPAGE
Signed-off-by: Sam James <sam@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Alfredo Tupone · gentoo
sci-mathematics/why3: Fix sa_handler signature
Closes: https://bugs.gentoo.org/944186 Signed-off-by: Alfredo Tupone <tupone@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Alfredo Tupone · gentoo
sci-mathematics/why3: add 1.7.2
Signed-off-by: Alfredo Tupone <tupone@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
sci-mathematics/why3: drop old 1.5.1
Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Maciej Barć · gentoo
sci-mathematics/why3: drop old 1.4.1-r1
Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
sci-mathematics/why3: drop old 1.5.0-r1
Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Maciej Barć · gentoo
sci-mathematics/why3: drop old 1.4.0-r3
Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Maciej Barć · gentoo
sci-mathematics/why3: bump to 1.6.0
Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
sci-mathematics/why3: bump to 1.5.1
Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Michael Mair-Keimberger · gentoo
sci-mathematics/why3: use https
Signed-off-by: Michael Mair-Keimberger <mmk@levelnine.at> Portage 3.0.34 / pkgdev 0.2.1 / pkgcheck 0.10.11 Signed-off-by: Alfredo Tupone <tupone@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
sci-mathematics/why3: remove unnecessary seq dependency
Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - François-Xavier Carton · gentoo
sci-mathematics/why3: bump to 1.5.0
Signed-off-by: François-Xavier Carton <fx.carton91@gmail.com> Closes: https://github.com/gentoo/gentoo/pull/25372 Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
sci-mathematics/why3: increase required menhir version
this is a very minor change to keep it in sync with https://opam.ocaml.org/packages/why3 also, no bump is needed since 20170418 version is long gone from ::gentoo Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
sci-mathematics/why3: bump to 1.4.1
Package-Manager: Portage-3.0.30, Repoman-3.0.3 Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - François-Xavier Carton · gentoo
sci-mathematics/why3: fix race condition in parallel make doc
"make doc" uses sphinx to build both latex and html documentation. Both sphinx rules in the makefile include "-d doc/.doctrees", ie. the same path for "the cached environment and doctree files". In a parallel make build, the rules are called simulateously, which means the cached files could be read by one process while they are still being written by the other. Closes: https://bugs.gentoo.org/831168 Signed-off-by: François-Xavier Carton <fx.carton91@gmail.com> Closes: https://github.com/gentoo/gentoo/pull/23802 Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - François-Xavier Carton · gentoo
sci-mathematics/why3: add missing latex dependencies
Closes: https://bugs.gentoo.org/828997 Closes: https://github.com/gentoo/gentoo/pull/23774 Signed-off-by: François-Xavier Carton <fx.carton91@gmail.com> Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
sci-mathematics/why3: fix *DEPEND
Closes: https://bugs.gentoo.org/828974 Package-Manager: Portage-3.0.28, Repoman-3.0.3 Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
sci-mathematics/why3: new package; add version 1.4.0
Move from ::guru to ::gentoo, add François-Xavier Carton as a co-maintainer. Package-Manager: Portage-3.0.28, Repoman-3.0.3 Signed-off-by: Maciej Barć <xgqt@gentoo.org>