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/j4ixs6zvp6m279jsws9wc2mvq12a3qad-coq-core-8.16.1.drv | ||
riscv64-linux | /gnu/store/vbd60rg40ffcr7d114kxdwjpw5mpkl17-coq-core-8.16.1.drv | ||
powerpc-linux | /gnu/store/n2s12zfdiql2q9x54bl9s1j6f78rdjy9-coq-core-8.16.1.drv | ||
powerpc64le-linux | /gnu/store/w1i0dbd0dmvisl9pws1ffbl8ifljnip6-coq-core-8.16.1.drv | ||
mips64el-linux | /gnu/store/47pd96m2pcwgj03vdy3b7brgf3drbk2g-coq-core-8.16.1.drv | ||
i686-linux | /gnu/store/s1fsxypgph5hyrmfn2sny5xlwnkjm9k4-coq-core-8.16.1.drv | ||
i586-gnu | /gnu/store/mwsb6zn94rl6k4z2scm3hwh6ybvhzxyq-coq-core-8.16.1.drv | ||
armhf-linux | /gnu/store/v0629l81irx6vpzsipqz84q5ix6zkms2-coq-core-8.16.1.drv | ||
aarch64-linux | /gnu/store/91rnisbhz73cnmrinz371s0pk85dsizd-coq-core-8.16.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 |