Revision 75a520cca62ea105a6fbb7f1d74b3a4ef439cd73

Language
View JSON

Package: coq-flocq @ 4.0.0

Synopsis

Floating-point formalization for the Coq system

Description

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.

Home page
https://flocq.gitlabpages.inria.fr
Location
gnu/packages/coq.scm (line: 230, column: 2)
License

Derivations

SystemTargetDerivationBuild status
x86_64-linux/gnu/store/ik0973zrsg8588qrx5hm8fl1gd6g3bvc-coq-flocq-4.0.0.drv
x86_64-linuxx86_64-w64-mingw32/gnu/store/mf222zhrcif04dpf5yx2g2jmmkfrkwzm-coq-flocq-4.0.0.drv
x86_64-linuxriscv64-linux-gnu/gnu/store/f34hayhhc7iszqpmsxrayy8lr5cvl93b-coq-flocq-4.0.0.drv
x86_64-linuxpowerpc-linux-gnu/gnu/store/kjfdvfn7jfmb6bn87b10hbnxq3khlp5h-coq-flocq-4.0.0.drv
x86_64-linuxpowerpc64le-linux-gnu/gnu/store/n52zfwjirdszii13sz69lxyhwcy34ikl-coq-flocq-4.0.0.drv
x86_64-linuxmips64el-linux-gnu/gnu/store/4pjh07sw56lqzg948syc03n29wh3zxg9-coq-flocq-4.0.0.drv
x86_64-linuxi686-w64-mingw32/gnu/store/6171x4x61h22y74s90f2z1bxp5lirrnj-coq-flocq-4.0.0.drv
x86_64-linuxi586-pc-gnu/gnu/store/5y1lynvzd1hjafhg49wgkh5aszmx02bs-coq-flocq-4.0.0.drv
x86_64-linuxarm-linux-gnueabihf/gnu/store/544qba73csw37zb310c4rfhk4qps3s1w-coq-flocq-4.0.0.drv
x86_64-linuxaarch64-linux-gnu/gnu/store/galphcsxlm4zmgy3kvi4avn9719m3nfv-coq-flocq-4.0.0.drv
riscv64-linux/gnu/store/vmx9xywd6g8n5gmcnwz02qg9qkd47f3m-coq-flocq-4.0.0.drv
    powerpc-linux/gnu/store/cxc7j590cla51n37mvq15xyfdgsvhd06-coq-flocq-4.0.0.drv
      powerpc64le-linux/gnu/store/sh7hriiy1bpb7847a529xjigp0sp8y85-coq-flocq-4.0.0.drv
      mips64el-linux/gnu/store/5ppmp7gb782is9p215yv21v0pgk3242s-coq-flocq-4.0.0.drv
        i686-linux/gnu/store/aidf4r94z968wbxmc657x227cgxr01fs-coq-flocq-4.0.0.drv
        i586-gnu/gnu/store/r99b96pd5ngl3a8pbygc4xj88g6dmnd9-coq-flocq-4.0.0.drv
        armhf-linux/gnu/store/wf2q7ma122j30hj4k9allb74bk8s7r4x-coq-flocq-4.0.0.drv
        aarch64-linux/gnu/store/x5di5qqfqbqqxjjxif8zq4waa3klphg1-coq-flocq-4.0.0.drv

        Lint warnings

        LinterMessageLocation
        optional-tests

        Make sure tests are only run when requested

        		the 'check' phase should respect #:tests?