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/ks8cx3f16mxg7444ydj1ddy85fbbjzyg-coq-flocq-3.3.1.drv | ||
x86_64-linux | i586-pc-gnu | /gnu/store/xlj258ncsrdvxwvy5r8rhdbsc70k28yk-coq-flocq-3.3.1.drv | |
x86_64-linux | arm-linux-gnueabihf | /gnu/store/bnfq3amz39s6gxb9ajvczal9yzakyhk9-coq-flocq-3.3.1.drv | |
x86_64-linux | aarch64-linux-gnu | /gnu/store/adbriaa0y21rd918py3vvqi9p91id6a9-coq-flocq-3.3.1.drv | |
powerpc64le-linux | /gnu/store/0haswhra8gxv860wp7syjn0qva8d07jw-coq-flocq-3.3.1.drv | ||
mips64el-linux | /gnu/store/7ii1answf7bjbcd2zzhsi4ia20qsxild-coq-flocq-3.3.1.drv | ||
i686-linux | /gnu/store/d5vp80z9p85fmz1h036m11l3r447l6c0-coq-flocq-3.3.1.drv | ||
i586-gnu | /gnu/store/cr3h3y6kwn665g7yfxq1j5hf749l6dq8-coq-flocq-3.3.1.drv | ||
armhf-linux | /gnu/store/v1jr4n5c57hkh3f36isc7xcaib1jypk2-coq-flocq-3.3.1.drv | ||
aarch64-linux | /gnu/store/hx6bqbhrmrhc6b07687zw2fqvi0id79v-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? |