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
v2023.12.13-r2 :: 0 :: gentoo
- Modified
- License
- GPL-3
- Keywords
- ~amd64 ~arm64
- USE flags
- coq doc emacs gtk html hypothesis-selection ocamlopt sexp zarith zip
v2021-r1 :: 0 :: gentoo
- Modified
- License
- GPL-3
- Keywords
- amd64
- USE flags
- coq doc emacs gtk html hypothesis-selection ocamlopt sexp 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
- Add support for x11-libs/gtk+ (The GIMP Toolkit)
- html
- Build HTML documentation
- hypothesis-selection
- Enable hypothesis selection
- ocamlopt
- Enable ocamlopt support (ocaml native code compiler) -- Produces faster programs (Warning: you have to disable/enable it at a global scale)
- sexp
- Add support for outputting S-expressions with dev-ml/ppx_sexp_conv
- 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 / yojson : JSON parsing and pretty-printing library for OCaml
dev-ml / zarith : Arithmetic and logic operations over arbitrary-precision integers
dev-tex / hevea : HeVeA is a quite complete and fast LaTeX to HTML translator
sci-mathematics / coq : Coq/Rocq is a proof assistant written in O'Caml
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 / yojson : JSON parsing and pretty-printing library for OCaml
dev-ml / zarith : Arithmetic and logic operations over arbitrary-precision integers
dev-tex / hevea : HeVeA is a quite complete and fast LaTeX to HTML translator
sci-mathematics / coq : Coq/Rocq is a proof assistant written in O'Caml
Depending packages
dev-lang / spark : Software development for high-reliability applications
sci-mathematics / why3 : Platform for deductive program verification
Change logs
- Repository mirror & CI · gentoo
Merge updates from master - Alfredo Tupone · gentoo
sci-mathematics/why3-for-spark: fix configure
Closes: https://bugs.gentoo.org/949519 Signed-off-by: Alfredo Tupone <tupone@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Alfredo Tupone · gentoo
sci-mathematics/why3-for-spark: fix for spark
Signed-off-by: Alfredo Tupone <tupone@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Alfredo Tupone · gentoo
sci-mathematics/why3-for-spark: keyword 2023.12.13-r1 for ~arm64
Signed-off-by: Alfredo Tupone <tupone@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Alfredo Tupone · gentoo
sci-mathematics/why3-for-spark: requires older coq
Signed-off-by: Alfredo Tupone <tupone@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Alfredo Tupone · gentoo
sci-mathematics/why3-for-spark: add 2023.12.13
Signed-off-by: Alfredo Tupone <tupone@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Sam James · gentoo
sci-mathematics/why3-for-spark: update HOMEPAGE
Signed-off-by: Sam James <sam@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Alfredo Tupone · gentoo
sci-mathematics/why3-for-spark: VariableOrderWrong
Signed-off-by: Alfredo Tupone <tupone@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Alfredo Tupone · gentoo
sci-mathematics/why3-for-spark: require ocamlopt
Closes: https://bugs.gentoo.org/913497 Signed-off-by: Alfredo Tupone <tupone@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Alfredo Tupone · gentoo
sci-mathematics/why3-for-spark: disable shuffle
Closes: https://bugs.gentoo.org/883167 Signed-off-by: Alfredo Tupone <tupone@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Alfredo Tupone · gentoo
sci-mathematics/why3-for-spark: drop 2020
Signed-off-by: Alfredo Tupone <tupone@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Alfredo Tupone · gentoo
sci-mathematics/why3-for-spark: stabilize 2021-r1 for amd64
Signed-off-by: Alfredo Tupone <tupone@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Alfredo Tupone · gentoo
sci-mathematics/why3-for-spark: drop 2019-r3
Signed-off-by: Alfredo Tupone <tupone@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Alfredo Tupone · gentoo
sci-mathematics/why3-for-spark: stabilize 2020 for amd64
Signed-off-by: Alfredo Tupone <tupone@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Alfredo Tupone · gentoo
sci-mathematics/why3-for-spark: require lablgtk-2
Signed-off-by: Alfredo Tupone <tupone@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Alfredo Tupone · gentoo
sci-mathematics/why3-for-spark: stop using <sci-mathematics/coq-8.12
Signed-off-by: Alfredo Tupone <tupone@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Michael Mair-Keimberger · gentoo
sci-mathematics/why3-for-spark: use https
Signed-off-by: Michael Mair-Keimberger <mmk@levelnine.at> Portage 3.0.34 / pkgdev 0.2.1 / pkgcheck 0.10.11 Closes: https://github.com/gentoo/gentoo/pull/26610 Signed-off-by: Alfredo Tupone <tupone@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Alfredo Tupone · gentoo
sci-mathematics/why3-for-spark: refix QA_FLAGS
Closes: https://bugs.gentoo.org/854555 Package-Manager: Portage-3.0.30, Repoman-3.0.3 Signed-off-by: Alfredo Tupone <tupone@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Alfredo Tupone · gentoo
sci-mathematics/why3-for-spark: ignore some QA warnings
Closes: https://bugs.gentoo.org/837278 Package-Manager: Portage-3.0.30, Repoman-3.0.3 Signed-off-by: Alfredo Tupone <tupone@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Alfredo Tupone · gentoo
sci-mathematics/why3-for-spark: add USE to select sexp
Closes: https://bugs.gentoo.org/834881 Package-Manager: Portage-3.0.30, Repoman-3.0.3 Signed-off-by: Alfredo Tupone <tupone@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Alfredo Tupone · gentoo
sci-mathematics/why3-for-spark: ignore CFLAGS
Closes: https://bugs.gentoo.org/799245 Package-Manager: Portage-3.0.30, Repoman-3.0.3 Signed-off-by: Alfredo Tupone <tupone@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Alfredo Tupone · gentoo
sci-mathematics/why3-for-spark: works with new ocaml too
Package-Manager: Portage-3.0.30, Repoman-3.0.3 Signed-off-by: Alfredo Tupone <tupone@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Alfredo Tupone · gentoo
sci-mathematics/why3-for-spark: duplicate deps
Package-Manager: Portage-3.0.30, Repoman-3.0.3 Signed-off-by: Alfredo Tupone <tupone@gentoo.org> - Alfredo Tupone · gentoo
sci-mathematics/why3-for-spark: fix doc deps
Package-Manager: Portage-3.0.30, Repoman-3.0.3 Signed-off-by: Alfredo Tupone <tupone@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Alfredo Tupone · gentoo
sci-mathematics/why3-for-spark: drop old version
Package-Manager: Portage-3.0.30, Repoman-3.0.3 Signed-off-by: Alfredo Tupone <tupone@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Alfredo Tupone · gentoo
sci-mathematics/why3-for-spark: UnusedInherits
Package-Manager: Portage-3.0.20, Repoman-3.0.3 Signed-off-by: Alfredo Tupone <tupone@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Alfredo Tupone · gentoo
sci-mathematics/why3-for-spark: enabled hypothesis-selection
Package-Manager: Portage-3.0.20, Repoman-3.0.2 Signed-off-by: Alfredo Tupone <tupone@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Alfredo Tupone · gentoo
sci-mathematics/why3-for-spark: disable hypothesis-selection
Closes: https://bugs.gentoo.org/799173 Package-Manager: Portage-3.0.20, Repoman-3.0.2 Signed-off-by: Alfredo Tupone <tupone@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Alfredo Tupone · gentoo
sci-mathematics/why3-for-spark: version bump to 2021
Package-Manager: Portage-3.0.18, Repoman-3.0.2 Signed-off-by: Alfredo Tupone <tupone@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Alfredo Tupone · gentoo
sci-mathematics/why3-for-spark: fix dep
Closes: https://bugs.gentoo.org/769845 Package-Manager: Portage-3.0.13, Repoman-3.0.2 Signed-off-by: Alfredo Tupone <tupone@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Alfredo Tupone · gentoo
sci-mathematics/why3-for-spark: version bump to 2020
Package-Manager: Portage-3.0.13, Repoman-3.0.2 Signed-off-by: Alfredo Tupone <tupone@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Jakov Smolic · gentoo
sci-mathematics/why3-for-spark: Remove old
Signed-off-by: Jakov Smolic <jakov.smolic@sartura.hr> Signed-off-by: David Seifert <soap@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Sam James · gentoo
sci-mathematics/why3-for-spark: update OCaml deps
* We need := for OCaml deps to ensure we're rebuilt when they update for consistency, to prevent strange issues. * Use ocamlopt= rather than ocamlopt? in the dev-lang/ocaml dependency to ensure ocamlopt is consistently on/off throughout the system. Package-Manager: Portage-3.0.12.0.2-prefix, Repoman-3.0.2 Signed-off-by: Sam James <sam@gentoo.org> - Sam James · gentoo
sci-mathematics/why3-for-spark: supports both lablgtk:2, :3 for most versions
See: https://gitlab.inria.fr/why3/why3/-/blob/master/CHANGES.md#version-121-october-28-2019 Package-Manager: Portage-3.0.12.0.2-prefix, Repoman-3.0.2 Signed-off-by: Sam James <sam@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Alfredo Tupone · gentoo
sci-mathematics/why3-for-spark: fix broken links
Closes: https://bugs.gentoo.org/728334 Package-Manager: Portage-2.3.99, Repoman-2.3.22 Signed-off-by: Alfredo Tupone <tupone@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Alfredo Tupone · gentoo
sci-mathematics/why3-for-spark: fix broken symlink
Closes: https://bugs.gentoo.org/728176 Package-Manager: Portage-2.3.99, Repoman-2.3.22 Signed-off-by: Alfredo Tupone <tupone@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Alfredo Tupone · gentoo
sci-mathematics/why3-for-spark: fix flags and compression
Closes: https://bugs.gentoo.org/728032 Closes: https://bugs.gentoo.org/728050 Package-Manager: Portage-2.3.99, Repoman-2.3.22 Signed-off-by: Alfredo Tupone <tupone@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Tupone Alfredo · gentoo
sci-mathematics/why3-for-spark: profiling is not more supported by newer ocaml
Package-Manager: Portage-2.3.79, Repoman-2.3.16 Signed-off-by: Alfredo Tupone <tupone@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Tupone Alfredo · gentoo
sci-mathematics/why3-for-spark: depend on a newer dev-ml/lablgtk
Package-Manager: Portage-2.3.79, Repoman-2.3.16 Signed-off-by: Alfredo Tupone <tupone@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Tupone Alfredo · gentoo
sci-mathematics/why3-for-spark: Needs a newer coq version
Package-Manager: Portage-2.3.79, Repoman-2.3.16 Signed-off-by: Alfredo Tupone <tupone@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Tupone Alfredo · gentoo
sci-mathematics/why3-for-spark: use ocaml-4.09
Closes: https://bugs.gentoo.org/705072 Package-Manager: Portage-2.3.79, Repoman-2.3.16 Signed-off-by: Alfredo Tupone <tupone@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Ulrich Müller · gentoo
sci-mathematics/why3-for-spark: Update virtual/emacs dependency.
The virtual is deprecated, depend on app-editors/emacs instead. Package-Manager: Portage-2.3.82, Repoman-2.3.20 Signed-off-by: Ulrich Müller <ulm@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Tupone Alfredo · gentoo
sci-mathematics/why3-for-spark: version bump to 2019
Package-Manager: Portage-2.3.69, Repoman-2.3.16 Signed-off-by: Alfredo Tupone <tupone@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Tupone Alfredo · gentoo
sci-mathematics/why3-for-spark: use virtual/emacs on dependency
Closes: https://bugs.gentoo.org/680312 Signed-off-by: Alfredo Tupone <tupone@gentoo.org> Package-Manager: Portage-2.3.51, Repoman-2.3.11 - Repository mirror & CI · gentoo
Merge updates from master - Tupone Alfredo · gentoo
sci-mathematics/why3-for-spark: Stable
Signed-off-by: Alfredo Tupone <tupone@gentoo.org> Package-Manager: Portage-2.3.51, Repoman-2.3.11 - Repository mirror & CI · gentoo
Merge updates from master - Tupone Alfredo · gentoo
sci-mathematics/why3-for-spark: Version bump to 2018
Package-Manager: Portage-2.3.40, Repoman-2.3.9 - Tupone Alfredo · gentoo
sci-mathematics/why3-for-spark: Fix STRIP_MASK usage. Bug #651458
Package-Manager: Portage-2.3.24, Repoman-2.3.6 - Tupone Alfredo · gentoo
sci-mathematics/why3-for-spark: dev-ml/camlzip-1.06 causes problem.
Package-Manager: Portage-2.3.8, Repoman-2.3.3 - Tupone Alfredo · gentoo
sci-mathematics/why3-for-spark: Add ocamlopt use flag
Package-Manager: Portage-2.3.8, Repoman-2.3.3 - Tupone Alfredo · gentoo
sci-mathematics/why3-for-spark: Install libraries
Package-Manager: Portage-2.3.8, Repoman-2.3.3 - Tupone Alfredo · gentoo
sci-mathematics/why3-for-spark: Enable coq tactics
Package-Manager: Portage-2.3.8, Repoman-2.3.3 - Tupone Alfredo · gentoo
sci-mathematics/why3-for-spark: remove extra --disable-zip
Package-Manager: Portage-2.3.8, Repoman-2.3.3 - Tupone Alfredo · gentoo
sci-mathematics/why3-for-spark: Add zip use flags
Package-Manager: Portage-2.3.8, Repoman-2.3.3 - Tupone Alfredo · gentoo
sci-mathematics/why3-for-spark: Adding examples
Package-Manager: Portage-2.3.8, Repoman-2.3.3 - Tupone Alfredo · gentoo
sci-mathematics/why3-for-spark: Fix SRC_URI
Package-Manager: Portage-2.3.8, Repoman-2.3.3 - Tupone Alfredo · gentoo
sci-mathematics/why3-for-spark: Adding why3 for spark
Package-Manager: Portage-2.3.8, Repoman-2.3.3