Install this package:
emerge -a sci-mathematics/kind2
If the package is masked, you can unmask it using the autounmask tool or standard emerge options:
autounmask sci-mathematics/kind2
Or alternatively:
emerge --autounmask-write -a sci-mathematics/kind2
| Version | EAPI | Keywords | Slot |
|---|---|---|---|
| 1.9.0 | 8 | ~amd64 | 0/1.9.0 |
<pkgmetadata>
<maintainer type="project">
<email>ml@gentoo.org</email>
<name>ML</name>
</maintainer>
<maintainer type="project">
<email>sci-mathematics@gentoo.org</email>
<name>Gentoo Mathematics Project</name>
</maintainer>
<longdescription>
Kind 2 is an open-source, multi-engine, SMT-based automatic model checker
for safety properties of finite-state or infinite-state synchronous
reactive systems expressed as in an extension of the Lustre language. In
its basic configuration it takes as input one or more Lustre files
annotated with properties to be proven invariant, and outputs for each
property either a confirmation or a counterexample, i.e., a sequence inputs
that falsifies the property. More advanced features include contract-based
compositional verification, proof generation for proven properties, and
contract-based test generation.
</longdescription>
<upstream>
<bugs-to>https://github.com/kind2-mc/kind2/issues/</bugs-to>
<remote-id type="github">kind2-mc/kind2</remote-id>
</upstream>
</pkgmetadata>
Manage flags for this package:
euse -i <flag> -p sci-mathematics/kind2 |
euse -E <flag> -p sci-mathematics/kind2 |
euse -D <flag> -p sci-mathematics/kind2
| Flag | Description | 1.9.0 |
|---|---|---|
| ocamlopt | Enable ocamlopt support (ocaml native code compiler) -- Produces faster programs (Warning: you have to disable/enable it at a global scale) | ⊕ |
| test | Enable dependencies and/or preparations necessary to run tests (usually controlled by FEATURES=test but can be toggled independently) | ✓ |
| Type | File | Size | Versions |
|---|---|---|---|
| DIST | kind2-1.9.0.tar.gz | 2009655 bytes | 1.9.0 |
| Type | File | Size |
|---|