sci-mathematics / why3-for-spark

Platform for deductive program verification

Official package sites : http://why3.lri.fr/ ·

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.

v2018 :: 0 :: gentoo

Modified
License
GPL-3
Keywords
amd64
USE flags
coq doc emacs gtk html hypothesis-selection ocamlopt profiling zarith zip

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)
profiling
Enable profiling
zarith
Use dev-ml/zarith
zip
Enable compression of session files

app-portage / elt-patches : Collection of patches for libtool.eclass

dev-lang / ocaml : Type-inferring functional programming language descended from the ML family

dev-ml / camlzip : Compressed file access ML library (ZIP, GZIP and JAR)

dev-ml / lablgtk : Objective CAML interface for Gtk+2

dev-ml / menhir : LR(1) parser generator for the OCaml language

dev-ml / ocamlgraph : O'Caml Graph library

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

dev-tex / rubber : A LaTeX wrapper for automatically building documents

sci-mathematics / coq : Proof assistant written in O'Caml

sys-devel / autoconf : Used to create autoconfiguration files

sys-devel / automake : Used to generate Makefile.in from Makefile.am

sys-devel / libtool : A shared library tool for developers

virtual / emacs : Virtual for GNU Emacs

dev-lang / ocaml : Type-inferring functional programming language descended from the ML family

dev-ml / camlzip : Compressed file access ML library (ZIP, GZIP and JAR)

dev-ml / lablgtk : Objective CAML interface for Gtk+2

dev-ml / menhir : LR(1) parser generator for the OCaml language

dev-ml / ocamlgraph : O'Caml Graph library

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

dev-tex / rubber : A LaTeX wrapper for automatically building documents

sci-mathematics / coq : Proof assistant written in O'Caml

virtual / emacs : Virtual for GNU Emacs

dev-lang / spark : Software development for high-reliability applications.

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