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/13pdzvndzfkpv807w3d9gwpx2gg69xv8-coq-core-8.14.1.drv | ||
riscv64-linux | /gnu/store/ci3h6d98qdf11j8nlyn7kg0r5cl24cfq-coq-core-8.14.1.drv | ||
powerpc-linux | /gnu/store/7aa8fz1bwm6fhvppkqx559pqh1xzxyvl-coq-core-8.14.1.drv | ||
powerpc64le-linux | /gnu/store/rfl4mrd35xjphaa9if57qrl1flwshbmw-coq-core-8.14.1.drv | ||
mips64el-linux | /gnu/store/0hw9l4d2a02n2kb8ml9ws0i38apzk95j-coq-core-8.14.1.drv | ||
i686-linux | /gnu/store/bbvik48khfiqkbaw41rr2x1i2v3riwif-coq-core-8.14.1.drv | ||
i586-gnu | /gnu/store/2m142rsmv6ish7g554dg043rjdjyck2m-coq-core-8.14.1.drv | ||
armhf-linux | /gnu/store/zs7h1n8zgsad9p6j3x869pgk3zlw0q3h-coq-core-8.14.1.drv | ||
aarch64-linux | /gnu/store/5jz9spd41ikrf2xiayz1y8zhs0728qsd-coq-core-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 |