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/9mnyqz7kl95vkrfx22n7aby49j0zcmxn-coq-flocq-3.4.2.drv | ||
x86_64-linux | i586-pc-gnu | /gnu/store/xcmvzvih89j724fr9ahx5bblxjjk14m2-coq-flocq-3.4.2.drv | |
x86_64-linux | arm-linux-gnueabihf | /gnu/store/6ws5mfq8wlf1hl3jh8mkga9bqxwv7i91-coq-flocq-3.4.2.drv | |
x86_64-linux | aarch64-linux-gnu | /gnu/store/nrsbha5ckak0wp4fci4kn2aj4phvhkkb-coq-flocq-3.4.2.drv | |
riscv64-linux | /gnu/store/wi630x0v9qni2a4108a29a0a1sl1xdbi-coq-flocq-3.4.2.drv | ||
powerpc-linux | /gnu/store/kchkhnk5p6v9yh75mibvz35lip1r0n0z-coq-flocq-3.4.2.drv | ||
powerpc64le-linux | /gnu/store/985xxxvyhyz8q853i9jyzqdyg8yrcl72-coq-flocq-3.4.2.drv | ||
mips64el-linux | /gnu/store/2kw22vx311gdd48r98ymh0gbjgrlq4aj-coq-flocq-3.4.2.drv | ||
i686-linux | /gnu/store/mf686zgsmc0rjddmnxh4vp3r04zvancv-coq-flocq-3.4.2.drv | ||
i586-gnu | /gnu/store/x2b29dmxp6dzhcxh3cgr5s4a1w2a945y-coq-flocq-3.4.2.drv | ||
armhf-linux | /gnu/store/38xf7qfy3kqbzk5gxss98vbilzkf72gg-coq-flocq-3.4.2.drv | ||
aarch64-linux | /gnu/store/2bznxb74p79cdzsc6bkgflpha1f750nd-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? |