Revision 6faac6a31a9a9ebf009427564103f7839ff35c77

Language
View JSON

Package: coq-flocq @ 4.1.4

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: 212, column: 2)
License

Derivations

SystemTargetDerivationBuild status
x86_64-linux/gnu/store/mvmjq6ilfdbnngcs7zi6szqvnjrcy4ig-coq-flocq-4.1.4.drv
x86_64-linuxxtensa-ath9k-elf/gnu/store/f9cwzz2cnlqd7ry2g70kv872g6yd006r-coq-flocq-4.1.4.drv
    x86_64-linuxx86_64-w64-mingw32/gnu/store/pys0hfl6xg57rnrn9hx81gshkxjgfxky-coq-flocq-4.1.4.drv
    x86_64-linuxx86_64-pc-gnu/gnu/store/96yv45z31zn06yfws42c7j1l6rm7kd8p-coq-flocq-4.1.4.drv
    x86_64-linuxx86_64-linux-gnux32/gnu/store/2xjc4wci8dxjfizz0knv0p65jvnqjmsy-coq-flocq-4.1.4.drv
      x86_64-linuxriscv64-linux-gnu/gnu/store/21fsb2y2s03qascjcx319nv57y2pk608-coq-flocq-4.1.4.drv
      x86_64-linuxpowerpc-linux-gnu/gnu/store/yffj2m0rzwrl6vzqinqzdcwmpfvkqlmh-coq-flocq-4.1.4.drv
        x86_64-linuxpowerpc64-linux-gnu/gnu/store/7wxp8viqncjg8p13zsn65iak5jgfk4km-coq-flocq-4.1.4.drv
          x86_64-linuxpowerpc64le-linux-gnu/gnu/store/p0j1ncwcl08rf2xym65iwwcf8ggkfwhk-coq-flocq-4.1.4.drv
          x86_64-linuxor1k-elf/gnu/store/plwpjxrfy5mk1qyi08n1sc9khkg2kc38-coq-flocq-4.1.4.drv
            x86_64-linuxmips64el-linux-gnu/gnu/store/b0b3cgf26x18lv34zz2m00g4kfqgbfyi-coq-flocq-4.1.4.drv
              x86_64-linuxloongarch64-linux-gnu/gnu/store/yqk5qr91dqfkcdvc4bnmkvfa6s0y27ks-coq-flocq-4.1.4.drv
              x86_64-linuxi686-w64-mingw32/gnu/store/xfl8i8q5841h5c0hjx98mxcq2cr6zgg3-coq-flocq-4.1.4.drv
                x86_64-linuxi586-pc-gnu/gnu/store/k7dk6gs1cnj2gja547fqc544xkdj8psv-coq-flocq-4.1.4.drv
                x86_64-linuxavr/gnu/store/k7j360bnza55aykkfrw4701hirswfqpg-coq-flocq-4.1.4.drv
                  x86_64-linuxarm-linux-gnueabihf/gnu/store/dz43w4g5y4zjh7gjs3ymj3zdx3jgk5zc-coq-flocq-4.1.4.drv
                  x86_64-linuxaarch64-linux-gnu/gnu/store/pkm34kg6n02pq0h1c1bb1gxxgwv317dn-coq-flocq-4.1.4.drv
                  x86_64-gnu/gnu/store/nni7239wqr3l2hmhvkl4wblq418975ql-coq-flocq-4.1.4.drv
                    riscv64-linux/gnu/store/jzvf36s2dnmiq8f5gwxll6idq7n3hj04-coq-flocq-4.1.4.drv
                    powerpc-linux/gnu/store/1w11xazfx3kvfr6x3br2hn4sxdc6g0gf-coq-flocq-4.1.4.drv
                      powerpc64le-linux/gnu/store/2n99mr17q6fkk7hgifdfdd363xdg1hgj-coq-flocq-4.1.4.drv
                      mips64el-linux/gnu/store/l2lz0xjx0067lq8kq9xl8l2nisvkhbyj-coq-flocq-4.1.4.drv
                        i686-linux/gnu/store/f5ngs4l8p5zfcnyx1bqfz38sx60r44al-coq-flocq-4.1.4.drv
                        i586-gnu/gnu/store/p8bk81qniiz0575s3drqsgq0shxi3ivp-coq-flocq-4.1.4.drv
                          armhf-linux/gnu/store/7r6wb638spzbi8paj5mqzhmg7am6dvjc-coq-flocq-4.1.4.drv
                          aarch64-linux/gnu/store/1133glgnxjk5rygdhghqadbczg2ilwsx-coq-flocq-4.1.4.drv

                          Lint warnings

                          LinterMessageLocation
                          optional-tests

                          Make sure tests are only run when requested

                          		the 'check' phase should respect #:tests?