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/5nc09nwi4b0svyyjbn41rz55c3z9ywzm-coq-ide-8.14.1.drv | ||
| powerpc-linux | /gnu/store/rpwa92kdin0w3rji8yqf2l2lcd2ff03x-coq-ide-8.14.1.drv | ||
| powerpc64le-linux | /gnu/store/11b7yxzmjn9fplimz0yp9d1x8ynj0v0v-coq-ide-8.14.1.drv | ||
| mips64el-linux | /gnu/store/pvjaw0h3w4ywx1y0fiqlfwdkyb594n0j-coq-ide-8.14.1.drv | ||
| i686-linux | /gnu/store/k881jqfawikgismqxridcslxyam5di6f-coq-ide-8.14.1.drv | ||
| i586-gnu | /gnu/store/f3r2lfg5bva0vs1w9fc73s2wxms0pxd6-coq-ide-8.14.1.drv | ||
| armhf-linux | /gnu/store/3h9zp95giry3j22jjmg97hvad40bmy2v-coq-ide-8.14.1.drv | ||
| aarch64-linux | /gnu/store/72dyfargcrs73zf2xakgshv9jg1gldrw-coq-ide-8.14.1.drv |
| Linter | Message | Location |
|---|---|---|
| input-labels Identify input labels that do not match package names | label 'lablgtk3' does not match package name 'lablgtk' | |
| patch-file-names Validate file names and availability of patches | file names of patches should start with the package name |