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/3dqyg2sjv2g1wf5xkiqrgzxmic60067w-coq-ide-8.14.1.drv | ||
riscv64-linux | /gnu/store/ffw4rfjn7s72cjjd32w4rvxw9h6f0kmi-coq-ide-8.14.1.drv | ||
powerpc-linux | /gnu/store/r9havjb8k0kzza42lcmcyis5lbi6fx97-coq-ide-8.14.1.drv | ||
powerpc64le-linux | /gnu/store/7z0sa1fpynkavr356jzgdvm06djr6v8x-coq-ide-8.14.1.drv | ||
mips64el-linux | /gnu/store/jpf9kl0nwmghipjdcmp7ysx5na4gbh5x-coq-ide-8.14.1.drv | ||
i686-linux | /gnu/store/62q6a4jzraxdykq1xib4lsba9jx411w6-coq-ide-8.14.1.drv | ||
i586-gnu | /gnu/store/gyss8zzdb73v00awri69jdk7q1l958n2-coq-ide-8.14.1.drv | ||
armhf-linux | /gnu/store/154wnbilp7f1nhfmndsjn584ai9cvb3b-coq-ide-8.14.1.drv | ||
aarch64-linux | /gnu/store/pl2iw0hckdd5pvq6xcrrjk1i6sg6b9ji-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' |