Language

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/9agas5h0sx393jxb3522m07dnairjlxm-coq-flocq-4.0.0.drv
    x86_64-linuxx86_64-w64-mingw32/gnu/store/h5g04fy8261dsr89xiky1cld1ccilb1c-coq-flocq-4.0.0.drv
      x86_64-linuxriscv64-linux-gnu/gnu/store/3adkh62mn8rsfplc44z1yzbf3r1br35z-coq-flocq-4.0.0.drv
        x86_64-linuxpowerpc-linux-gnu/gnu/store/2aw7qk8a7q2f4758nldjrpzdv8g2y70a-coq-flocq-4.0.0.drv
          x86_64-linuxpowerpc64le-linux-gnu/gnu/store/sgrz5av4125p21cqklcd90nz6kw65211-coq-flocq-4.0.0.drv
            x86_64-linuxmips64el-linux-gnu/gnu/store/s66dqr5hc82f80x8b775zar2fcnnb0bz-coq-flocq-4.0.0.drv
              x86_64-linuxi686-w64-mingw32/gnu/store/1wz9pjy88cd8i3gyarsxgbysflncryqs-coq-flocq-4.0.0.drv
                x86_64-linuxi586-pc-gnu/gnu/store/ygcwn2725b4vbs3bm5p1aszjxjniqagc-coq-flocq-4.0.0.drv
                  x86_64-linuxarm-linux-gnueabihf/gnu/store/k9vg7xyqvm0c57cgv6c39mz7yywr1252-coq-flocq-4.0.0.drv
                    x86_64-linuxaarch64-linux-gnu/gnu/store/vbz1vva8cykggap3pvfmxfifybaflvcn-coq-flocq-4.0.0.drv
                      riscv64-linux/gnu/store/zj95z1g05drzqmdb7zyih211zpa9jryc-coq-flocq-4.0.0.drv
                        powerpc-linux/gnu/store/qlxnhzv4pp2ff4b35gznzwmi25hv9xcj-coq-flocq-4.0.0.drv
                          powerpc64le-linux/gnu/store/y96vgzs2h1vwc1syir388gjr1kb8nr7p-coq-flocq-4.0.0.drv
                            mips64el-linux/gnu/store/vskxpccgdydgasmgq2qlqk2clwj8byv0-coq-flocq-4.0.0.drv
                              i686-linux/gnu/store/b67iah6zkzaaxjfzsn6gz21nqvfch6sj-coq-flocq-4.0.0.drv
                                i586-gnu/gnu/store/88ah2899s8q75svf76j8frchnmd1r4sd-coq-flocq-4.0.0.drv
                                  armhf-linux/gnu/store/h4alhljbpdq3rdypzhq3hgx2gjzigmw8-coq-flocq-4.0.0.drv
                                    aarch64-linux/gnu/store/nl3xhz9glgiyl60brqgzl2bqhpw9njdr-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?
                                      derivation

                                      Report failure to compile a package to a derivation

                                      failed to create i586-gnu derivation: #<&package-input-error package: #<package nghttp2@1.48.0 gnu/packages/web.scm:7487 7f8ed7409c60> input: ("_" "static")>
                                      derivation

                                      Report failure to compile a package to a derivation

                                      failed to create i586-gnu derivation: #<&package-input-error package: #<package nghttp2@1.48.0 gnu/packages/web.scm:7487 7fa7aa068c60> input: ("_" "static")>
                                      derivation

                                      Report failure to compile a package to a derivation

                                      failed to create i586-gnu derivation: #<&package-input-error package: #<package nghttp2@1.48.0 gnu/packages/web.scm:7487 7f5755cb9c60> input: ("_" "static")>
                                      derivation

                                      Report failure to compile a package to a derivation

                                      failed to create i586-gnu derivation: #<&package-input-error package: #<package nghttp2@1.48.0 gnu/packages/web.scm:7487 7f119da52c60> input: ("_" "static")>