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/0yvkglg2bvq6fs4ya33dx3bzh1fvl3c8-coq-flocq-3.4.2.drv | ||
x86_64-linux | i586-pc-gnu | /gnu/store/8k1igax9p4a57k9vs78qqq50qrqp5psw-coq-flocq-3.4.2.drv | |
x86_64-linux | arm-linux-gnueabihf | /gnu/store/3f8yyz966700jyz290gsgs8hir85qzjh-coq-flocq-3.4.2.drv | |
x86_64-linux | aarch64-linux-gnu | /gnu/store/s5adxhjip5g0q0kczf4rajlranpd3sr9-coq-flocq-3.4.2.drv | |
riscv64-linux | /gnu/store/ar5ihsjpf87rjvbj6cwdpk8kzh6b6z1k-coq-flocq-3.4.2.drv | ||
powerpc-linux | /gnu/store/dma2s6ni5cvc31b79wrvrz370vnn7538-coq-flocq-3.4.2.drv | ||
powerpc64le-linux | /gnu/store/pcv9dfqjk839k3g4j6ksdlcddh41h928-coq-flocq-3.4.2.drv | ||
mips64el-linux | /gnu/store/zh3fwcrqsdfkdx6w46kdxm32ygcj9im4-coq-flocq-3.4.2.drv | ||
i686-linux | /gnu/store/vymbmzk5bzxknqjwn1vypz7xfssigbil-coq-flocq-3.4.2.drv | ||
i586-gnu | /gnu/store/2wiwi9gmpk6yyngsm7ixismzjpy1i32m-coq-flocq-3.4.2.drv | ||
armhf-linux | /gnu/store/dsmb7gl7r9y5hgwcrwbviycbcbi40b2n-coq-flocq-3.4.2.drv | ||
aarch64-linux | /gnu/store/z7nnjjlqxzsysnyhn0amhjq5a0nq4ryn-coq-flocq-3.4.2.drv |
Linter | Message | Location |
---|---|---|
optional-tests Make sure tests are only run when requested | the 'check' phase should respect #:tests? |