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/i62v0w0pn1m9d9d23hmclwxgni4m032h-coq-ide-8.15.2.drv | ||
| aarch64-linux | /gnu/store/g98qnh9q2wna9pcq7hzz5zjyps4x81pd-coq-ide-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 | |
| input-labels Identify input labels that do not match package names | label 'lablgtk3' does not match package name 'lablgtk' | |
| derivation Report failure to compile a package to a derivation | failed to create i586-gnu derivation: #<&package-input-error package: #<package nghttp2@1.48.0 gnu/packages/web.scm:7487 7f8ed7409c60> input: ("_" "static")> | |
| derivation Report failure to compile a package to a derivation | failed to create i586-gnu derivation: #<&package-input-error package: #<package nghttp2@1.48.0 gnu/packages/web.scm:7487 7fa7aa068c60> input: ("_" "static")> | |
| derivation Report failure to compile a package to a derivation | failed to create i586-gnu derivation: #<&package-input-error package: #<package nghttp2@1.48.0 gnu/packages/web.scm:7487 7f5755cb9c60> input: ("_" "static")> | |
| derivation Report failure to compile a package to a derivation | failed to create i586-gnu derivation: #<&package-input-error package: #<package nghttp2@1.48.0 gnu/packages/web.scm:7487 7f119da52c60> input: ("_" "static")> |