<!DOCTYPE html>
<html lang="en">
  <head>
    <meta charset="utf-8">
    <meta name="viewport" content="width=device-width, initial-scale=1">
    <title>flocq: 5 m 35 s 🏆</title>
    <link rel="shortcut icon" type="image/png" href="../../../../../favicon.png" />
    <link href="../../../../../bootstrap.min.css" rel="stylesheet">
    <link href="../../../../../bootstrap-custom.css" rel="stylesheet">
    <link href="//maxcdn.bootstrapcdn.com/font-awesome/4.2.0/css/font-awesome.min.css" rel="stylesheet">
    <script src="../../../../../moment.min.js"></script>
    <!-- HTML5 Shim and Respond.js IE8 support of HTML5 elements and media queries -->
    <!-- WARNING: Respond.js doesn't work if you view the page via file:// -->
    <!--[if lt IE 9]>
      <script src="https://oss.maxcdn.com/html5shiv/3.7.2/html5shiv.min.js"></script>
      <script src="https://oss.maxcdn.com/respond/1.4.2/respond.min.js"></script>
    <![endif]-->
  </head>
  <body>
    <div class="container">
      <div class="navbar navbar-default" role="navigation">
        <div class="container-fluid">
          <div class="navbar-header">
            <a class="navbar-brand" href="../../../../.."><i class="fa fa-lg fa-flag-checkered"></i> Coq bench</a>
          </div>
          <div id="navbar" class="collapse navbar-collapse">
            <ul class="nav navbar-nav">
              <li><a href="../..">clean / released</a></li>
              <li class="active"><a href="">8.13.0 / flocq - 3.4.3</a></li>
            </ul>
          </div>
        </div>
      </div>
      <div class="article">
        <div class="row">
          <div class="col-md-12">
            <a href="../..">« Up</a>
            <h1>
              flocq
              <small>
                3.4.3
                <span class="label label-success">5 m 35 s 🏆</span>
              </small>
            </h1>
            <p>📅 <em><script>document.write(moment("2022-03-08 23:52:51 +0000", "YYYY-MM-DD HH:mm:ss Z").fromNow());</script> (2022-03-08 23:52:51 UTC)</em><p>
            <h2>Context</h2>
            <pre># Packages matching: installed
# Name                # Installed # Synopsis
base-bigarray         base
base-threads          base
base-unix             base
conf-findutils        1           Virtual package relying on findutils
conf-gmp              4           Virtual package relying on a GMP lib system installation
coq                   8.13.0      Formal proof management system
num                   1.4         The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml                 4.12.1      The OCaml compiler (virtual package)
ocaml-base-compiler   4.12.1      Official release 4.12.1
ocaml-config          2           OCaml Switch Configuration
ocaml-options-vanilla 1           Ensure that OCaml is compiled with no special options enabled
ocamlfind             1.9.3       A library manager for OCaml
zarith                1.12        Implements arithmetic and logical operations over arbitrary-precision integers
# opam file:
opam-version: &quot;2.0&quot;
maintainer: &quot;guillaume.melquiond@inria.fr&quot;
homepage: &quot;https://flocq.gitlabpages.inria.fr/&quot;
dev-repo: &quot;git+https://gitlab.inria.fr/flocq/flocq.git&quot;
bug-reports: &quot;https://gitlab.inria.fr/flocq/flocq/issues&quot;
license: &quot;LGPL-3.0-or-later&quot;
build: [
  [&quot;autoconf&quot;] {dev}
  [&quot;./configure&quot;]
  [&quot;./remake&quot; &quot;-j%{jobs}%&quot;]
]
install: [&quot;./remake&quot; &quot;install&quot;]
depends: [
  &quot;coq&quot; {&gt;= &quot;8.7&quot; &amp; &lt; &quot;8.16~&quot;}
  &quot;conf-autoconf&quot; {build &amp; dev}
  (&quot;conf-g++&quot; {build} | &quot;conf-clang&quot; {build})
]
tags: [
  &quot;keyword:floating-point arithmetic&quot;
  &quot;logpath:Flocq&quot;
  &quot;date:2022-01-17&quot;
]
authors: [
  &quot;Sylvie Boldo &lt;sylvie.boldo@inria.fr&gt;&quot;
  &quot;Guillaume Melquiond &lt;guillaume.melquiond@inria.fr&gt;&quot;
]
synopsis: &quot;A formalization of floating-point arithmetic for the Coq system&quot;
url {
  src: &quot;https://flocq.gitlabpages.inria.fr/releases/flocq-3.4.3.tar.gz&quot;
  checksum: &quot;sha512=10f407e91e0d601b502b2c89104a8753dfcc3d9572f0fd9d007c7692d3d6c96fd5652fb103bcf2396a64236947734ee725c01f4ba2901565f9da38667f538d5a&quot;
}
</pre>
            <h2>Lint</h2>
            <dl class="dl-horizontal">
              <dt>Command</dt>
              <dd><code>true</code></dd>
              <dt>Return code</dt>
              <dd>0</dd>
            </dl>
            <h2>Dry install 🏜️</h2>
            <p>Dry install with the current Coq version:</p>
            <dl class="dl-horizontal">
              <dt>Command</dt>
              <dd><code>opam install -y --show-action coq-flocq.3.4.3 coq.8.13.0</code></dd>
              <dt>Return code</dt>
              <dd>0</dd>
            </dl>
            <p>Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:</p>
            <dl class="dl-horizontal">
              <dt>Command</dt>
              <dd><code>true</code></dd>
              <dt>Return code</dt>
              <dd>0</dd>
            </dl>
            <h2>Install dependencies</h2>
            <dl class="dl-horizontal">
              <dt>Command</dt>
              <dd><code>opam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-flocq.3.4.3 coq.8.13.0</code></dd>
              <dt>Return code</dt>
              <dd>0</dd>
              <dt>Duration</dt>
              <dd>10 s</dd>
            </dl>
            <h2>Install 🚀</h2>
            <dl class="dl-horizontal">
              <dt>Command</dt>
              <dd><code>opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-flocq.3.4.3 coq.8.13.0</code></dd>
              <dt>Return code</dt>
              <dd>0</dd>
              <dt>Duration</dt>
              <dd>5 m 35 s</dd>
            </dl>
            <h2>Installation size</h2>
            <p>Total: 9 M</p>
            <ul>
              <li>3 M <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Pff/Pff.vo</code></li>
              <li>1 M <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Pff/Pff.v</code></li>
              <li>518 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Prop/Double_rounding.vo</code></li>
              <li>475 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/IEEE754/BinarySingleNaN.vo</code></li>
              <li>468 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/IEEE754/Binary.vo</code></li>
              <li>222 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Pff/Pff2Flocq.vo</code></li>
              <li>208 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Core/Ulp.vo</code></li>
              <li>166 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Core/Raux.vo</code></li>
              <li>165 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Core/Generic_fmt.vo</code></li>
              <li>154 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Prop/Double_rounding.v</code></li>
              <li>137 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Prop/Div_sqrt_error.vo</code></li>
              <li>130 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Calc/Round.vo</code></li>
              <li>116 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Prop/Round_odd.vo</code></li>
              <li>116 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/IEEE754/Bits.vo</code></li>
              <li>113 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Core/Round_pred.vo</code></li>
              <li>103 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Core/Digits.vo</code></li>
              <li>103 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Prop/Relative.vo</code></li>
              <li>103 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/IEEE754/BinarySingleNaN.v</code></li>
              <li>95 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/IEEE754/Binary.v</code></li>
              <li>93 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Pff/Pff2FlocqAux.vo</code></li>
              <li>89 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Core/Zaux.vo</code></li>
              <li>88 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Calc/Bracket.vo</code></li>
              <li>85 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Pff/Pff2Flocq.v</code></li>
              <li>81 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Core/FLT.vo</code></li>
              <li>80 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/IEEE754/PrimFloat.vo</code></li>
              <li>76 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Prop/Plus_error.vo</code></li>
              <li>74 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Core/Round_NE.vo</code></li>
              <li>68 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Core/Ulp.v</code></li>
              <li>66 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Core/FLX.vo</code></li>
              <li>61 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Prop/Mult_error.vo</code></li>
              <li>59 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Core/Float_prop.vo</code></li>
              <li>57 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Core/FTZ.vo</code></li>
              <li>53 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Core/Generic_fmt.v</code></li>
              <li>53 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Calc/Div.vo</code></li>
              <li>51 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Calc/Sqrt.vo</code></li>
              <li>49 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Core/Raux.v</code></li>
              <li>43 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Calc/Operations.vo</code></li>
              <li>42 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Prop/Sterbenz.vo</code></li>
              <li>36 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Core/FIX.vo</code></li>
              <li>35 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Core/Defs.vo</code></li>
              <li>35 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Core/Round_pred.v</code></li>
              <li>32 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Prop/Round_odd.v</code></li>
              <li>31 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Calc/Round.v</code></li>
              <li>30 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Prop/Div_sqrt_error.v</code></li>
              <li>29 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Prop/Relative.v</code></li>
              <li>29 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Core/Core.vo</code></li>
              <li>27 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Core/Digits.v</code></li>
              <li>24 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Pff/Pff2FlocqAux.v</code></li>
              <li>21 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/IEEE754/Bits.v</code></li>
              <li>19 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Core/Zaux.v</code></li>
              <li>19 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/IEEE754/SpecFloatCompat.vo</code></li>
              <li>17 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Calc/Bracket.v</code></li>
              <li>17 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Prop/Plus_error.v</code></li>
              <li>14 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Core/Round_NE.v</code></li>
              <li>14 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Version.vo</code></li>
              <li>13 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/IEEE754/PrimFloat.v</code></li>
              <li>13 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Core/FLT.v</code></li>
              <li>12 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Core/Float_prop.v</code></li>
              <li>10 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Prop/Mult_error.v</code></li>
              <li>9 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Core/FLX.v</code></li>
              <li>8 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Core/FTZ.v</code></li>
              <li>5 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Calc/Sqrt.v</code></li>
              <li>5 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Calc/Div.v</code></li>
              <li>4 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Prop/Sterbenz.v</code></li>
              <li>4 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Calc/Operations.v</code></li>
              <li>2 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Core/Defs.v</code></li>
              <li>2 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Core/FIX.v</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Version.v</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/Core/Core.v</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Flocq/IEEE754/SpecFloatCompat.v</code></li>
            </ul>
            <h2>Uninstall 🧹</h2>
            <dl class="dl-horizontal">
              <dt>Command</dt>
              <dd><code>opam remove -y coq-flocq.3.4.3</code></dd>
              <dt>Return code</dt>
              <dd>0</dd>
              <dt>Missing removes</dt>
              <dd>
                none
              </dd>
              <dt>Wrong removes</dt>
              <dd>
                none
              </dd>
            </dl>
          </div>
        </div>
      </div>
      <hr/>
      <div class="footer">
        <p class="text-center">
          Sources are on <a href="https://github.com/coq-bench">GitHub</a> © Guillaume Claret 🐣
        </p>
      </div>
    </div>
    <script src="https://ajax.googleapis.com/ajax/libs/jquery/1.11.1/jquery.min.js"></script>
    <script src="../../../../../bootstrap.min.js"></script>
  </body>
</html>
