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/8sjsdzxsrc9nb6dfk29nryrlyb1b6wlr-coq-ide-8.15.0.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 |