Floating-point formalization for the Coq system
Flocq (Floats for Coq) is a floating-point formalization for the Coq system. It provides a comprehensive library of theorems on a multi-radix multi-precision arithmetic. It also supports efficient numerical computations inside Coq.
System | Target | Derivation | Build status |
---|---|---|---|
x86_64-linux | /gnu/store/s69fwdfn54b2l5fb9dmgkr5k2a3pdq2f-coq-flocq-3.3.1.drv | ||
x86_64-linux | i586-pc-gnu | /gnu/store/lqf3habqgqy7g9za4al980cv7px9hxli-coq-flocq-3.3.1.drv | |
x86_64-linux | arm-linux-gnueabihf | /gnu/store/01shaxp9b9r2pv8cc0dsyaj0b3fp8ia4-coq-flocq-3.3.1.drv | |
x86_64-linux | aarch64-linux-gnu | /gnu/store/nl873kqkfjh6y3783sq77fn2d3zdrixw-coq-flocq-3.3.1.drv | |
powerpc64le-linux | /gnu/store/qmm3lf9lx4qc5bb4i61mhp889ja3j4xs-coq-flocq-3.3.1.drv | ||
mips64el-linux | /gnu/store/xsw0fa01ziqv9z8j5050n8wyd4wvwdlm-coq-flocq-3.3.1.drv | ||
i686-linux | /gnu/store/aq2ngv3lag3rgirn2k4r9hwal0f1vn7r-coq-flocq-3.3.1.drv | ||
i586-gnu | /gnu/store/l41vpfsvnjgy8nydlrxnhcw8s1ad0zq6-coq-flocq-3.3.1.drv | ||
armhf-linux | /gnu/store/g8k3v6bfpmyxs8iyn2b0xpgjv9vjismy-coq-flocq-3.3.1.drv | ||
aarch64-linux | /gnu/store/qy45anm3in602r61af7vkmfny3anbq2v-coq-flocq-3.3.1.drv |
Linter | Message | Location |
---|---|---|
optional-tests Make sure tests are only run when requested | the 'check' phase should respect #:tests? |