Proof assistant for higher-order logic
Coq is a proof assistant for higher-order logic, which allows the development of computer programs consistent with their formal specification. It is developed using Objective Caml and Camlp5.
| System | Target | Derivation | Build status |
|---|---|---|---|
| x86_64-linux | /gnu/store/0iaws8l2wqdfbcp42vwns3h49dkfinmy-coq-core-8.15.1.drv | ||
| riscv64-linux | /gnu/store/z49g452fhblhpny162f0p7sril4nvzd4-coq-core-8.15.1.drv | ||
| powerpc-linux | /gnu/store/rxyvdrsxkxi5axc05fj3zm15gnc9kj49-coq-core-8.15.1.drv | ||
| powerpc64le-linux | /gnu/store/brjz8dzc56iqabm5bk7qgc3g0fp112sk-coq-core-8.15.1.drv | ||
| mips64el-linux | /gnu/store/h0q120gbl74mfkj71p3jrxkbc0wf2sag-coq-core-8.15.1.drv | ||
| i686-linux | /gnu/store/5q18x70972fqj323mmg3cqyp2rypnq08-coq-core-8.15.1.drv | ||
| i586-gnu | /gnu/store/fplm9piqxsqjdxnb0lws0xnkb4rfbji1-coq-core-8.15.1.drv | ||
| armhf-linux | /gnu/store/5bghl3x2why4wbbidy8f3dwq1h7zys7g-coq-core-8.15.1.drv | ||
| aarch64-linux | /gnu/store/m4fixlljs2gscxy8lwchfq5rxfr3slva-coq-core-8.15.1.drv |
| Linter | Message | Location |
|---|---|---|
| patch-file-names Validate file names and availability of patches | file names of patches should start with the package name |