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/h21c9afg94jgki98zpvnsmjsnh1yc1ry-coq-flocq-3.3.1.drv | ||
x86_64-linux | i586-pc-gnu | /gnu/store/95z0w570dr0ngglz8p40jky9dnlnr6jb-coq-flocq-3.3.1.drv | |
x86_64-linux | arm-linux-gnueabihf | /gnu/store/6mvs50ax91j8acc4r9bf6zp6adaxxqgd-coq-flocq-3.3.1.drv | |
x86_64-linux | aarch64-linux-gnu | /gnu/store/8323vwjk9iss81syqmdf38157a23m509-coq-flocq-3.3.1.drv | |
powerpc64le-linux | /gnu/store/rm8c0kd9i462hqhgiqwsxff0z111ys45-coq-flocq-3.3.1.drv | ||
mips64el-linux | /gnu/store/d8lfjm6pky1yh9g6rjpf3flmyhn8idpv-coq-flocq-3.3.1.drv | ||
i686-linux | /gnu/store/b150sn783w2jh37pq09x6w28vb5ar8n2-coq-flocq-3.3.1.drv | ||
i586-gnu | /gnu/store/1f704yidnhc44n34p5cw679sw8ddbybv-coq-flocq-3.3.1.drv | ||
armhf-linux | /gnu/store/p7fkd49jd4yml8chz5v2kj0rbiwnnplm-coq-flocq-3.3.1.drv | ||
aarch64-linux | /gnu/store/j9jpzsjwfmf6cp8dasg70q9894rlchkk-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? |