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/aq81gykz069384rp6254lkbn38qvd8zj-coq-flocq-3.3.1.drv | ||
| x86_64-linux | i586-pc-gnu | /gnu/store/kygd3s5v2qvngpc5cadkxwyavry6dqn8-coq-flocq-3.3.1.drv | |
| x86_64-linux | arm-linux-gnueabihf | /gnu/store/xzbp5avqck1j7sghi4awbaaz6zxkc219-coq-flocq-3.3.1.drv | |
| x86_64-linux | aarch64-linux-gnu | /gnu/store/d9lv5v2xkw6cv5v58gy0b66axxy2vfxj-coq-flocq-3.3.1.drv | |
| powerpc64le-linux | /gnu/store/m419jmrlbqan1x4h8d2flg1ymmvh8vx5-coq-flocq-3.3.1.drv | ||
| mips64el-linux | /gnu/store/rsyr09p124wry3c6k80zv7wg17q2z0sp-coq-flocq-3.3.1.drv | ||
| i686-linux | /gnu/store/z0y2gj2w5pizw4fvm8v4pkj2spf2c1sw-coq-flocq-3.3.1.drv | ||
| i586-gnu | /gnu/store/lajapdinv4vwgaarv8r1n3jzmvia6sda-coq-flocq-3.3.1.drv | ||
| armhf-linux | /gnu/store/ylykb0ck87y0vz1fwivx5g8x767zrm76-coq-flocq-3.3.1.drv | ||
| aarch64-linux | /gnu/store/fvk38ax9b95n5sa0lna530zym7y6a3qq-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? |