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/3kgh8dsd70bznv557h7r7b5wmv43ykga-coq-ide-8.14.1.drv | ||
riscv64-linux | /gnu/store/01873f4ncrnscnarzzh254ydisshizc6-coq-ide-8.14.1.drv | ||
powerpc-linux | /gnu/store/g3fk7yzvvapdr91rxbjjawiy51s4hycp-coq-ide-8.14.1.drv | ||
powerpc64le-linux | /gnu/store/yh978frgninj6bjc4p07mac8pzn2c6sj-coq-ide-8.14.1.drv | ||
mips64el-linux | /gnu/store/lnsj7574sivsaj8y0nvg4dafm2il1gr9-coq-ide-8.14.1.drv | ||
i686-linux | /gnu/store/n9wxnxrhdlw7pw2bv690j7p3zn5cciq0-coq-ide-8.14.1.drv | ||
i586-gnu | /gnu/store/fjaxv5yyq0pbjy9q748jaxapa2kzb3pw-coq-ide-8.14.1.drv | ||
armhf-linux | /gnu/store/wmg9pb02f5av575crlwwafplrxxgcw02-coq-ide-8.14.1.drv | ||
aarch64-linux | /gnu/store/qhwnhbkh5n8i0qxmv05rmlw3jbg96bbs-coq-ide-8.14.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 | |
input-labels Identify input labels that do not match package names | label 'lablgtk3' does not match package name 'lablgtk' |