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/z8i6nzxm7p9aqlrml03sxcjmh4fk1ck1-coq-core-8.15.2.drv | ||
riscv64-linux | /gnu/store/3y0sq0vmhsx2jm6ydvwxb4p5bi6fv5dq-coq-core-8.15.2.drv | ||
powerpc-linux | /gnu/store/95mxjxb41aqi71d2xdfh55lji9mh0b29-coq-core-8.15.2.drv | ||
powerpc64le-linux | /gnu/store/ly9533rvma6h59mn27cvjsr17cnp5js8-coq-core-8.15.2.drv | ||
mips64el-linux | /gnu/store/9nrj6rs2glz199a40xwrai23q9gjys3r-coq-core-8.15.2.drv | ||
i686-linux | /gnu/store/p4p9qisgbbm59ksayw80knhwnclkmdzg-coq-core-8.15.2.drv | ||
i586-gnu | /gnu/store/4qh73zhknfn81r2yg0hlqxkmyxa96dxm-coq-core-8.15.2.drv | ||
armhf-linux | /gnu/store/w2rjsqbbmd74iird9rgf7avs5lxkynfq-coq-core-8.15.2.drv | ||
aarch64-linux | /gnu/store/1qzz60szdw4mbm06qvpfwagml0kv6rjl-coq-core-8.15.2.drv |
Linter | Message | Location |
---|---|---|
patch-file-names Validate file names and availability of patches | file names of patches should start with the package name |