Gentoo Packages

sci-mathematics/why3-for-spark (gentoo)

Search

Install

Install this package:

emerge -a sci-mathematics/why3-for-spark

If the package is masked, you can unmask it using the autounmask tool or standard emerge options:

autounmask sci-mathematics/why3-for-spark

Or alternatively:

emerge --autounmask-write -a sci-mathematics/why3-for-spark

Package Information

Description:
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.
Homepage:
https://www.why3.org/ https://github.com/AdaCore/why3
License:
GPL-3

Versions

Version EAPI Keywords Slot
2023.12.13-r2 8 amd64 ~arm64 0

Metadata

Description

Maintainers

Upstream

Raw Metadata XML 
<pkgmetadata>
	<maintainer type="project">
		<email>ada@gentoo.org</email>
	</maintainer>
	<longdescription lang="en">
		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.
	</longdescription>
	<use>
		<flag name="coq">Add <pkg>sci-mathematics/coq</pkg> support</flag>
		<flag name="html">Build HTML documentation</flag>
		<flag name="hypothesis-selection">Enable hypothesis selection</flag>
		<flag name="sexp">Add support for outputting S-expressions with <pkg>dev-ml/ppx_sexp_conv</pkg></flag>
		<flag name="zarith">Use Zarith (<pkg>dev-ml/zarith</pkg>) instead of Nums (<pkg>dev-ml/num</pkg>) for computations</flag>
		<flag name="zip">Enable compression of session files</flag>
	</use>
	<upstream>
		<remote-id type="github">AdaCore/why3</remote-id>
	</upstream>
</pkgmetadata>

Lint Warnings

USE Flags

Manage flags for this package: euse -i <flag> -p sci-mathematics/why3-for-spark | euse -E <flag> -p sci-mathematics/why3-for-spark | euse -D <flag> -p sci-mathematics/why3-for-spark

Flag Description 2023.12.13-r2
coq Add <pkg>sci-mathematics/coq</pkg> 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 <pkg>dev-ml/ppx_sexp_conv</pkg> ✓
zarith Use Zarith (<pkg>dev-ml/zarith</pkg>) instead of Nums (<pkg>dev-ml/num</pkg>) for computations ✓
zip Enable compression of session files ✓

Files

Manifest

Type File Size Versions
Unmatched Entries
Type File Size
DIST why3-for-spark-2023.12.13.tar.gz 7119379 bytes