package rocq-prover
Build not checkedInstall
dune-project
Dependency
Authors
Maintainers
Description
The Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
Typical applications include the certification of properties of programming languages (e.g. the CompCert compiler certification project, or the Bedrock verified low-level programming library), the formalization of mathematics (e.g. the full formalization of the Feit-Thompson theorem or homotopy type theory) and teaching.
This package is a virtual package gathering the rocq-core and rocq-stdlib packages.
Added to opam-repository:
Dependencies (2)
Dev Dependencies
None
Optional Dependencies
None
Used by (5)
-
coq-lsp
= "0.2.5+9.0" -
coq-waterproof
= "3.1.0+9.0" - lstar
- lstar-rocq
-
rocq-waterproof
< "3.1.1+9.1"
Conflicts
None
Build status
Results of building rocq-prover with each compiler on check.ci.ocaml.org, run of against opam-repository 78c202b. All results for this package.
Each result links to its build log. To keep crawlers from overloading the site, build logs require a GitHub sign-in (see ocurrent/opam-health-check). On your first log, GitHub asks you to “Authorize opam-health-check”, the OCurrent app that runs these checks; it sees only your public profile, not your repositories. The sign-in lasts 30 days.
This version is not in the latest run; the versions below are.
- good Package successfully built
- partial One of the dependencies failed to build
- bad Package failed to build
- n/a Package is not available in this environment
- internal Internal failure