<!DOCTYPE html>
<html lang="en">
  <head>
    <meta charset="utf-8">
    <meta name="viewport" content="width=device-width, initial-scale=1">
    <title>Coq bench</title>
    <link rel="shortcut icon" type="image/png" href="../../../../../favicon.png" />
    <link href="../../../../../bootstrap.min.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">
            <button type="button" class="navbar-toggle collapsed" data-toggle="collapse" data-target="#navbar" aria-expanded="false" aria-controls="navbar">
              <span class="sr-only">Toggle navigation</span>
              <span class="icon-bar"></span>
              <span class="icon-bar"></span>
              <span class="icon-bar"></span>
            </button>
            <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="../../..">Unstable</a></li>
              <li><a href=".">dev / contrib:float dev</a></li>
              <li class="active"><a href="">2014-12-17 17:32:45</a></li>
            </ul>
            <ul class="nav navbar-nav navbar-right">
              <li><a href="../../../../../about.html">About</a></li>
            </ul>
          </div>
        </div>
      </div>
      <div class="article">
        <div class="row">
          <div class="col-md-12">
            <a href=".">« Up</a>
            <h1>
              contrib:float
              <small>
                dev
                <span class="label label-success">1 m 0 s</span>
              </small>
            </h1>
            <p><em><script>document.write(moment("2014-12-17 17:32:45 +0000", "YYYY-MM-DD HH:mm:ss Z").fromNow());</script> (2014-12-17 17:32:45 UTC)</em><p>
            <h2>Lint</h2>
            <dl class="dl-horizontal">
              <dt>Command</dt>
              <dd><code>ruby lint.rb unstable ../unstable/packages/coq:contrib:float/coq:contrib:float.dev</code></dd>
              <dt>Return code</dt>
              <dd>0</dd>
              <dt>Duration</dt>
              <dd>0 s</dd>
              <dt>Output</dt>
              <dd><pre>The package is valid.
</pre></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 --dry-run coq:contrib:float.dev coq.dev</code></dd>
              <dt>Return code</dt>
              <dd>0</dd>
              <dt>Duration</dt>
              <dd>1 s</dd>
              <dt>Output</dt>
              <dd><pre>[NOTE] Package coq is already installed (current version is dev).
The following actions will be performed:
 - install   coq:contrib:float.dev
=== 1 to install ===
=-=- Synchronizing package archives -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
=-=- Installing packages =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
Building coq:contrib:float.dev:
  coq_makefile -f Make -o Makefile
  make -j4
  make install
Installing coq:contrib:float.dev.
</pre></dd>
            </dl>
            <p>Dry install without Coq, to test if the problem was incompatibility with the current Coq version:</p>
            <dl class="dl-horizontal">
              <dt>Command</dt>
              <dd><code>true</code></dd>
              <dt>Return code</dt>
              <dd>0</dd>
              <dt>Duration</dt>
              <dd>0 s</dd>
            </dl>
            <h2>Install dependencies</h2>
            <dl class="dl-horizontal">
              <dt>Command</dt>
              <dd><code>opam install -y --deps-only coq:contrib:float.dev</code></dd>
              <dt>Return code</dt>
              <dd>0</dd>
              <dt>Duration</dt>
              <dd>2 s</dd>
            </dl>
            <h2>Install</h2>
            <dl class="dl-horizontal">
              <dt>Command</dt>
              <dd><code>opam install -y --verbose coq:contrib:float.dev</code></dd>
              <dt>Return code</dt>
              <dd>0</dd>
              <dt>Duration</dt>
              <dd>1 m 0 s</dd>
              <dt>Output</dt>
              <dd><pre>The following actions will be performed:
 - install   coq:contrib:float.dev
=== 1 to install ===
=-=- Synchronizing package archives -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
[coq:contrib:float] Fetching https://gforge.inria.fr/git/coq-contribs/float.git#trunk
Initialized empty Git repository in /home/bench/.opam/packages.dev/coq:contrib:float.dev/.git/
[master (root-commit) ca98cdd] opam-git-init
From https://gforge.inria.fr/git/coq-contribs/float
 * [new branch]      trunk      -&gt; opam-ref
 * [new branch]      trunk      -&gt; origin/trunk
.cvsignore
AllFloat.v
Closest.v
Closest2Plus.v
Closest2Prop.v
ClosestMult.v
ClosestPlus.v
ClosestProp.v
Digit.v
FPred.v
FSucc.v
Faux.v
Fbound.v
Fcomp.v
Finduct.v
Float.v
Fmin.v
Fnorm.v
Fodd.v
Fop.v
Fprop.v
Fround.v
FroundMult.v
FroundPlus.v
FroundProp.v
LICENSE
MSB.v
MSBProp.v
Make
Makefile
Option.v
Paux.v
Power.v
README
Rpow.v
Zdivides.v
Zenum.v
description
sTactic.v
HEAD is now at 9426cad Revert &quot;Regenerating Makefiles.&quot; We will be able to do so when we have access
=-=- Installing packages =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
Building coq:contrib:float.dev:
  coq_makefile -f Make -o Makefile
  make -j4
  make install
&quot;coqdep&quot; -c -R &quot;.&quot; Float &quot;AllFloat.v&quot; &gt; &quot;AllFloat.v.d&quot; || ( RV=$?; rm -f &quot;AllFloat.v.d&quot;; exit ${RV} )
&quot;coqdep&quot; -c -R &quot;.&quot; Float &quot;Closest.v&quot; &gt; &quot;Closest.v.d&quot; || ( RV=$?; rm -f &quot;Closest.v.d&quot;; exit ${RV} )
&quot;coqdep&quot; -c -R &quot;.&quot; Float &quot;Closest2Plus.v&quot; &gt; &quot;Closest2Plus.v.d&quot; || ( RV=$?; rm -f &quot;Closest2Plus.v.d&quot;; exit ${RV} )
&quot;coqdep&quot; -c -R &quot;.&quot; Float &quot;Closest2Prop.v&quot; &gt; &quot;Closest2Prop.v.d&quot; || ( RV=$?; rm -f &quot;Closest2Prop.v.d&quot;; exit ${RV} )
&quot;coqdep&quot; -c -R &quot;.&quot; Float &quot;ClosestMult.v&quot; &gt; &quot;ClosestMult.v.d&quot; || ( RV=$?; rm -f &quot;ClosestMult.v.d&quot;; exit ${RV} )
&quot;coqdep&quot; -c -R &quot;.&quot; Float &quot;ClosestPlus.v&quot; &gt; &quot;ClosestPlus.v.d&quot; || ( RV=$?; rm -f &quot;ClosestPlus.v.d&quot;; exit ${RV} )
&quot;coqdep&quot; -c -R &quot;.&quot; Float &quot;ClosestProp.v&quot; &gt; &quot;ClosestProp.v.d&quot; || ( RV=$?; rm -f &quot;ClosestProp.v.d&quot;; exit ${RV} )
&quot;coqdep&quot; -c -R &quot;.&quot; Float &quot;Digit.v&quot; &gt; &quot;Digit.v.d&quot; || ( RV=$?; rm -f &quot;Digit.v.d&quot;; exit ${RV} )
&quot;coqdep&quot; -c -R &quot;.&quot; Float &quot;FPred.v&quot; &gt; &quot;FPred.v.d&quot; || ( RV=$?; rm -f &quot;FPred.v.d&quot;; exit ${RV} )
&quot;coqdep&quot; -c -R &quot;.&quot; Float &quot;FSucc.v&quot; &gt; &quot;FSucc.v.d&quot; || ( RV=$?; rm -f &quot;FSucc.v.d&quot;; exit ${RV} )
&quot;coqdep&quot; -c -R &quot;.&quot; Float &quot;Faux.v&quot; &gt; &quot;Faux.v.d&quot; || ( RV=$?; rm -f &quot;Faux.v.d&quot;; exit ${RV} )
&quot;coqdep&quot; -c -R &quot;.&quot; Float &quot;Fbound.v&quot; &gt; &quot;Fbound.v.d&quot; || ( RV=$?; rm -f &quot;Fbound.v.d&quot;; exit ${RV} )
&quot;coqdep&quot; -c -R &quot;.&quot; Float &quot;Fcomp.v&quot; &gt; &quot;Fcomp.v.d&quot; || ( RV=$?; rm -f &quot;Fcomp.v.d&quot;; exit ${RV} )
&quot;coqdep&quot; -c -R &quot;.&quot; Float &quot;Finduct.v&quot; &gt; &quot;Finduct.v.d&quot; || ( RV=$?; rm -f &quot;Finduct.v.d&quot;; exit ${RV} )
&quot;coqdep&quot; -c -R &quot;.&quot; Float &quot;Float.v&quot; &gt; &quot;Float.v.d&quot; || ( RV=$?; rm -f &quot;Float.v.d&quot;; exit ${RV} )
&quot;coqdep&quot; -c -R &quot;.&quot; Float &quot;Fmin.v&quot; &gt; &quot;Fmin.v.d&quot; || ( RV=$?; rm -f &quot;Fmin.v.d&quot;; exit ${RV} )
&quot;coqdep&quot; -c -R &quot;.&quot; Float &quot;Fnorm.v&quot; &gt; &quot;Fnorm.v.d&quot; || ( RV=$?; rm -f &quot;Fnorm.v.d&quot;; exit ${RV} )
&quot;coqdep&quot; -c -R &quot;.&quot; Float &quot;Fodd.v&quot; &gt; &quot;Fodd.v.d&quot; || ( RV=$?; rm -f &quot;Fodd.v.d&quot;; exit ${RV} )
&quot;coqdep&quot; -c -R &quot;.&quot; Float &quot;Fop.v&quot; &gt; &quot;Fop.v.d&quot; || ( RV=$?; rm -f &quot;Fop.v.d&quot;; exit ${RV} )
&quot;coqdep&quot; -c -R &quot;.&quot; Float &quot;Fprop.v&quot; &gt; &quot;Fprop.v.d&quot; || ( RV=$?; rm -f &quot;Fprop.v.d&quot;; exit ${RV} )
&quot;coqdep&quot; -c -R &quot;.&quot; Float &quot;Fround.v&quot; &gt; &quot;Fround.v.d&quot; || ( RV=$?; rm -f &quot;Fround.v.d&quot;; exit ${RV} )
&quot;coqdep&quot; -c -R &quot;.&quot; Float &quot;FroundMult.v&quot; &gt; &quot;FroundMult.v.d&quot; || ( RV=$?; rm -f &quot;FroundMult.v.d&quot;; exit ${RV} )
&quot;coqdep&quot; -c -R &quot;.&quot; Float &quot;FroundPlus.v&quot; &gt; &quot;FroundPlus.v.d&quot; || ( RV=$?; rm -f &quot;FroundPlus.v.d&quot;; exit ${RV} )
&quot;coqdep&quot; -c -R &quot;.&quot; Float &quot;FroundProp.v&quot; &gt; &quot;FroundProp.v.d&quot; || ( RV=$?; rm -f &quot;FroundProp.v.d&quot;; exit ${RV} )
&quot;coqdep&quot; -c -R &quot;.&quot; Float &quot;MSB.v&quot; &gt; &quot;MSB.v.d&quot; || ( RV=$?; rm -f &quot;MSB.v.d&quot;; exit ${RV} )
&quot;coqdep&quot; -c -R &quot;.&quot; Float &quot;MSBProp.v&quot; &gt; &quot;MSBProp.v.d&quot; || ( RV=$?; rm -f &quot;MSBProp.v.d&quot;; exit ${RV} )
&quot;coqdep&quot; -c -R &quot;.&quot; Float &quot;Option.v&quot; &gt; &quot;Option.v.d&quot; || ( RV=$?; rm -f &quot;Option.v.d&quot;; exit ${RV} )
&quot;coqdep&quot; -c -R &quot;.&quot; Float &quot;Paux.v&quot; &gt; &quot;Paux.v.d&quot; || ( RV=$?; rm -f &quot;Paux.v.d&quot;; exit ${RV} )
&quot;coqdep&quot; -c -R &quot;.&quot; Float &quot;Power.v&quot; &gt; &quot;Power.v.d&quot; || ( RV=$?; rm -f &quot;Power.v.d&quot;; exit ${RV} )
&quot;coqdep&quot; -c -R &quot;.&quot; Float &quot;Zdivides.v&quot; &gt; &quot;Zdivides.v.d&quot; || ( RV=$?; rm -f &quot;Zdivides.v.d&quot;; exit ${RV} )
&quot;coqdep&quot; -c -R &quot;.&quot; Float &quot;Zenum.v&quot; &gt; &quot;Zenum.v.d&quot; || ( RV=$?; rm -f &quot;Zenum.v.d&quot;; exit ${RV} )
&quot;coqdep&quot; -c -R &quot;.&quot; Float &quot;sTactic.v&quot; &gt; &quot;sTactic.v.d&quot; || ( RV=$?; rm -f &quot;sTactic.v.d&quot;; exit ${RV} )
&quot;coqdep&quot; -c -R &quot;.&quot; Float &quot;Rpow.v&quot; &gt; &quot;Rpow.v.d&quot; || ( RV=$?; rm -f &quot;Rpow.v.d&quot;; exit ${RV} )
&quot;coqc&quot;  -q  -R &quot;.&quot; Float   sTactic
&quot;coqc&quot;  -q  -R &quot;.&quot; Float   Option
&quot;coqc&quot;  -q  -R &quot;.&quot; Float   Faux
&quot;coqc&quot;  -q  -R &quot;.&quot; Float   Digit
&quot;coqc&quot;  -q  -R &quot;.&quot; Float   Zenum
&quot;coqc&quot;  -q  -R &quot;.&quot; Float   Rpow
&quot;coqc&quot;  -q  -R &quot;.&quot; Float   Paux
&quot;coqc&quot;  -q  -R &quot;.&quot; Float   Power
&quot;coqc&quot;  -q  -R &quot;.&quot; Float   Float
&quot;coqc&quot;  -q  -R &quot;.&quot; Float   Zdivides
&quot;coqc&quot;  -q  -R &quot;.&quot; Float   Fcomp
&quot;coqc&quot;  -q  -R &quot;.&quot; Float   Fop
&quot;coqc&quot;  -q  -R &quot;.&quot; Float   Fbound
&quot;coqc&quot;  -q  -R &quot;.&quot; Float   Fprop
&quot;coqc&quot;  -q  -R &quot;.&quot; Float   Fnorm
&quot;coqc&quot;  -q  -R &quot;.&quot; Float   MSB
&quot;coqc&quot;  -q  -R &quot;.&quot; Float   FSucc
&quot;coqc&quot;  -q  -R &quot;.&quot; Float   MSBProp
&quot;coqc&quot;  -q  -R &quot;.&quot; Float   FPred
&quot;coqc&quot;  -q  -R &quot;.&quot; Float   Fmin
&quot;coqc&quot;  -q  -R &quot;.&quot; Float   Finduct
&quot;coqc&quot;  -q  -R &quot;.&quot; Float   Fodd
&quot;coqc&quot;  -q  -R &quot;.&quot; Float   Fround
&quot;coqc&quot;  -q  -R &quot;.&quot; Float   FroundProp
&quot;coqc&quot;  -q  -R &quot;.&quot; Float   Closest
&quot;coqc&quot;  -q  -R &quot;.&quot; Float   FroundPlus
&quot;coqc&quot;  -q  -R &quot;.&quot; Float   FroundMult
&quot;coqc&quot;  -q  -R &quot;.&quot; Float   ClosestProp
&quot;coqc&quot;  -q  -R &quot;.&quot; Float   ClosestPlus
&quot;coqc&quot;  -q  -R &quot;.&quot; Float   Closest2Prop
&quot;coqc&quot;  -q  -R &quot;.&quot; Float   ClosestMult
&quot;coqc&quot;  -q  -R &quot;.&quot; Float   Closest2Plus
&quot;coqc&quot;  -q  -R &quot;.&quot; Float   AllFloat
cd &quot;.&quot; &amp;&amp; for i in Rpow.vo sTactic.vo Zenum.vo Zdivides.vo Power.vo Paux.vo Option.vo MSBProp.vo MSB.vo FroundProp.vo FroundPlus.vo FroundMult.vo Fround.vo Fprop.vo Fop.vo Fodd.vo Fnorm.vo Fmin.vo Float.vo Finduct.vo Fcomp.vo Fbound.vo Faux.vo FSucc.vo FPred.vo Digit.vo ClosestProp.vo ClosestPlus.vo ClosestMult.vo Closest2Prop.vo Closest2Plus.vo Closest.vo AllFloat.vo   ; do \
 install -d &quot;`dirname &quot;&quot;&quot;/home/bench/.opam/system/lib/coq/user-contrib&quot;/Float/$i`&quot;; \
 install -m 0644 $i &quot;&quot;&quot;/home/bench/.opam/system/lib/coq/user-contrib&quot;/Float/$i; \
done
Installing coq:contrib:float.dev.
</pre></dd>
            </dl>
            <h2>Installation size</h2>
            <p>Total: 2,524 K</p>
            <ul>
              <li>164 K <code>/home/bench/.opam/system/lib/coq/user-contrib/Float/FroundMult.vo</code></li>
              <li>161 K <code>/home/bench/.opam/system/lib/coq/user-contrib/Float/Fnorm.vo</code></li>
              <li>143 K <code>/home/bench/.opam/system/lib/coq/user-contrib/Float/Faux.vo</code></li>
              <li>143 K <code>/home/bench/.opam/system/lib/coq/user-contrib/Float/FroundProp.vo</code></li>
              <li>141 K <code>/home/bench/.opam/system/lib/coq/user-contrib/Float/Paux.vo</code></li>
              <li>128 K <code>/home/bench/.opam/system/lib/coq/user-contrib/Float/FSucc.vo</code></li>
              <li>118 K <code>/home/bench/.opam/system/lib/coq/user-contrib/Float/FroundPlus.vo</code></li>
              <li>103 K <code>/home/bench/.opam/system/lib/coq/user-contrib/Float/ClosestPlus.vo</code></li>
              <li>101 K <code>/home/bench/.opam/system/lib/coq/user-contrib/Float/ClosestProp.vo</code></li>
              <li>90 K <code>/home/bench/.opam/system/lib/coq/user-contrib/Float/Zdivides.vo</code></li>
              <li>87 K <code>/home/bench/.opam/system/lib/coq/user-contrib/Float/Fodd.vo</code></li>
              <li>85 K <code>/home/bench/.opam/system/lib/coq/user-contrib/Float/MSB.vo</code></li>
              <li>85 K <code>/home/bench/.opam/system/lib/coq/user-contrib/Float/ClosestMult.vo</code></li>
              <li>82 K <code>/home/bench/.opam/system/lib/coq/user-contrib/Float/Fmin.vo</code></li>
              <li>80 K <code>/home/bench/.opam/system/lib/coq/user-contrib/Float/FPred.vo</code></li>
              <li>69 K <code>/home/bench/.opam/system/lib/coq/user-contrib/Float/Float.vo</code></li>
              <li>67 K <code>/home/bench/.opam/system/lib/coq/user-contrib/Float/Closest.vo</code></li>
              <li>63 K <code>/home/bench/.opam/system/lib/coq/user-contrib/Float/Digit.vo</code></li>
              <li>63 K <code>/home/bench/.opam/system/lib/coq/user-contrib/Float/Fround.vo</code></li>
              <li>60 K <code>/home/bench/.opam/system/lib/coq/user-contrib/Float/Rpow.vo</code></li>
              <li>58 K <code>/home/bench/.opam/system/lib/coq/user-contrib/Float/Power.vo</code></li>
              <li>55 K <code>/home/bench/.opam/system/lib/coq/user-contrib/Float/Fbound.vo</code></li>
              <li>53 K <code>/home/bench/.opam/system/lib/coq/user-contrib/Float/Fop.vo</code></li>
              <li>50 K <code>/home/bench/.opam/system/lib/coq/user-contrib/Float/Fcomp.vo</code></li>
              <li>50 K <code>/home/bench/.opam/system/lib/coq/user-contrib/Float/Finduct.vo</code></li>
              <li>45 K <code>/home/bench/.opam/system/lib/coq/user-contrib/Float/Zenum.vo</code></li>
              <li>42 K <code>/home/bench/.opam/system/lib/coq/user-contrib/Float/Closest2Plus.vo</code></li>
              <li>33 K <code>/home/bench/.opam/system/lib/coq/user-contrib/Float/Fprop.vo</code></li>
              <li>30 K <code>/home/bench/.opam/system/lib/coq/user-contrib/Float/Closest2Prop.vo</code></li>
              <li>30 K <code>/home/bench/.opam/system/lib/coq/user-contrib/Float/MSBProp.vo</code></li>
              <li>23 K <code>/home/bench/.opam/system/lib/coq/user-contrib/Float/AllFloat.vo</code></li>
              <li>2 K <code>/home/bench/.opam/system/lib/coq/user-contrib/Float/Option.vo</code></li>
              <li>2 K <code>/home/bench/.opam/system/lib/coq/user-contrib/Float/sTactic.vo</code></li>
              <li>1 K <code>/home/bench/.opam/system/lib/coq:contrib:float/opam.config</code></li>
              <li>1 K <code>/home/bench/.opam/system/install/coq:contrib:float.install</code></li>
            </ul>
            <h2>Uninstall</h2>
            <dl class="dl-horizontal">
              <dt>Command</dt>
              <dd><code>opam remove -y coq:contrib:float.dev</code></dd>
              <dt>Return code</dt>
              <dd>0</dd>
              <dt>Duration</dt>
              <dd>2 s</dd>
              <dt>Output</dt>
              <dd><pre>The following actions will be performed:
 - remove    coq:contrib:float.dev
=== 1 to remove ===
=-=- Synchronizing package archives -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
[coq:contrib:float] Fetching https://gforge.inria.fr/git/coq-contribs/float.git#trunk
=-=- Removing Packages =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
Removing coq:contrib:float.dev.
  rm -R /home/bench/.opam/system/lib/coq/user-contrib/Float
</pre></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">
          <small>Sources are on <a href="https://github.com/coq-bench">GitHub</a>. © Guillaume Claret.</small>
        </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>