Gentoo Packages

Search

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

Metadata

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.

Maintainers

• Unknown (ada@gentoo.org) - Type: project

Upstream

• Remote IDs:
  • github: AdaCore/why3

<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

• [Warning] Ebuild 2023.12.13-r2 uses IUSE flag 'emacs' which is not documented in metadata.xml. Add the flag to metadata.xml <use> section.
• [Warning] Ebuild 2023.12.13-r2 uses IUSE flag 'gtk' which is not documented in metadata.xml. Add the flag to metadata.xml <use> section.
• [Warning] Ebuild 2023.12.13-r2 uses IUSE flag 'ocamlopt' which is not documented in metadata.xml. Add the flag to metadata.xml <use> section.
• [Warning] Missing md5-cache for version 2023.12.13-r2. Run 'ebuild <ebuild_file> manifest' or 'egencache' to generate it.

USE Flags

Files

• why3-for-spark-2020-bibtex.patch
• why3-for-spark-2020-gentoo.patch
• why3-for-spark-2021-make.patch
• why3-for-spark-2021-sighandler.patch
• why3-for-spark-2023.12.13-flags.patch
• why3-for-spark-2023.12.13-spark.patch
• why3-for-spark-2023.12.13-yojson3.patch

Manifest