Package coq-gappa @ 1.4.2

Synopsis

Verify and formally prove properties on numerical programs

Description

Gappa is a tool intended to help verifying and formally proving properties on numerical programs dealing with floating-point or fixed-point arithmetic. It has been used to write robust floating-point filters for CGAL and it is used to certify elementary functions in CRlibm. While Gappa is intended to be used directly, it can also act as a backend prover for the Why3 software verification plateform or as an automatic tactic for the Coq proof assistant.

Home page
https://gappa.gforge.inria.fr/
Location
gnu/packages/coq.scm (line: 266, column: 2)
Licenses

Lint warnings

LinterMessageLocation
derivation

Report failure to compile a package to a derivation

failed to create i686-linux derivation: path ‘/gnu/store/imq41gd3q2767il9gq6mqh5cv44x09rf-guile-2.2.6.drv’ is not valid
derivation

Report failure to compile a package to a derivation

failed to create armhf-linux derivation: path ‘/gnu/store/9wn798a6w534mnn4f28lglbjmib9n392-zlib-1.2.11.drv’ is not valid
derivation

Report failure to compile a package to a derivation

failed to create aarch64-linux derivation: path ‘/gnu/store/0afbxr7962z9ci6kw840n088qsmyz8lr-guile-2.2.6.drv’ is not valid
derivation

Report failure to compile a package to a derivation

failed to create mips64el-linux derivation: path ‘/gnu/store/aiwgcl5dppar2s8l408bshywjybsy3nd-zlib-1.2.11.drv’ is not valid
derivation

Report failure to compile a package to a derivation

failed to create x86_64-linux derivation: path ‘/gnu/store/1dz7hwpizsbvz88j1g2s4c16ayjy36dz-coq-8.10.2.drv’ is not valid