<!DOCTYPE html>
<html lang="en">
  <head>
    <meta charset="utf-8">
    <meta name="viewport" content="width=device-width, initial-scale=1">
    <title>mathcomp-analysis: 9 m 50 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.12.1 / mathcomp-analysis - 0.3.6</a></li>
            </ul>
          </div>
        </div>
      </div>
      <div class="article">
        <div class="row">
          <div class="col-md-12">
            <a href="../..">« Up</a>
            <h1>
              mathcomp-analysis
              <small>
                0.3.6
                <span class="label label-success">9 m 50 s 🏆</span>
              </small>
            </h1>
            <p>📅 <em><script>document.write(moment("2021-12-29 09:04:54 +0000", "YYYY-MM-DD HH:mm:ss Z").fromNow());</script> (2021-12-29 09:04:54 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
coq                 8.12.1      Formal proof management system
num                 1.4         The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml               4.10.2      The OCaml compiler (virtual package)
ocaml-base-compiler 4.10.2      Official release 4.10.2
ocaml-config        1           OCaml Switch Configuration
ocamlfind           1.9.1       A library manager for OCaml
# opam file:
opam-version: &quot;2.0&quot;
maintainer: &quot;Reynald Affeldt &lt;reynald.affeldt@aist.go.jp&gt;&quot;
homepage: &quot;https://github.com/math-comp/analysis&quot;
dev-repo: &quot;git+https://github.com/math-comp/analysis.git&quot;
bug-reports: &quot;https://github.com/math-comp/analysis/issues&quot;
license: &quot;CECILL-C&quot;
synopsis: &quot;An analysis library for mathematical components&quot;
description: &quot;&quot;&quot;
This repository contains an experimental library for real analysis for
the Coq proof-assistant and using the Mathematical Components library.&quot;&quot;&quot;
build: [make &quot;-j%{jobs}%&quot; ]
install: [make &quot;install&quot;]
depends: [
  &quot;coq&quot; { (&gt;= &quot;8.11&quot; &amp; &lt; &quot;8.14~&quot;) | (= &quot;dev&quot;) }
  &quot;coq-mathcomp-ssreflect&quot; { (&gt;= &quot;1.12.0&quot; &amp; &lt; &quot;1.13~&quot;) | (= &quot;dev&quot;) }
  &quot;coq-mathcomp-fingroup&quot; { (&gt;= &quot;1.12.0&quot; &amp; &lt; &quot;1.13~&quot;) | (= &quot;dev&quot;) }
  &quot;coq-mathcomp-algebra&quot; { (&gt;= &quot;1.12.0&quot; &amp; &lt; &quot;1.13~&quot;) | (= &quot;dev&quot;) }
  &quot;coq-mathcomp-solvable&quot; { (&gt;= &quot;1.12.0&quot; &amp; &lt; &quot;1.13~&quot;) | (= &quot;dev&quot;) }
  &quot;coq-mathcomp-field&quot; { (&gt;= &quot;1.12.0&quot; &amp; &lt; &quot;1.13~&quot;) | (= &quot;dev&quot;) }
  &quot;coq-mathcomp-finmap&quot; { (&gt;= &quot;1.5.1&quot; &amp; &lt; &quot;1.6~&quot;) | (= &quot;dev&quot;) }
  &quot;coq-mathcomp-bigenough&quot; { (&gt;= &quot;1.0.0&quot;) }
  &quot;coq-hierarchy-builder&quot; { (&gt;= &quot;0.10.0&quot; &amp; &lt; &quot;1.1.0&quot;) | (= &quot;dev&quot;) }
]
tags: [
  &quot;keyword:analysis&quot;
  &quot;keyword:topology&quot;
  &quot;keyword:real numbers&quot;
  &quot;date:2021-03-04&quot;
  &quot;logpath:mathcomp.analysis&quot;
]
authors: [
  &quot;Reynald Affeldt&quot;
  &quot;Cyril Cohen&quot;
  &quot;Marie Kerjean&quot;
  &quot;Assia Mahboubi&quot;
  &quot;Damien Rouhling&quot;
  &quot;Kazuhiko Sakaguchi&quot;
  &quot;Pierre-Yves Strub&quot;
]
url {
  http: &quot;https://github.com/math-comp/analysis/archive/0.3.6.tar.gz&quot;
  checksum: &quot;sha512=6f19f26bfdfeff6a9e56d27e278141c851cbbd5e584af523ef153b70b9326ab396ab8f582a56762e33a7053a4130b144feb4ba92a8acac62eb5e47193f3450a2&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-mathcomp-analysis.0.3.6 coq.8.12.1</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-mathcomp-analysis.0.3.6 coq.8.12.1</code></dd>
              <dt>Return code</dt>
              <dd>0</dd>
              <dt>Duration</dt>
              <dd>55 m 2 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-mathcomp-analysis.0.3.6 coq.8.12.1</code></dd>
              <dt>Return code</dt>
              <dd>0</dd>
              <dt>Duration</dt>
              <dd>9 m 50 s</dd>
            </dl>
            <h2>Installation size</h2>
            <p>Total: 15 M</p>
            <ul>
              <li>1 M <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/normedtype.vo</code></li>
              <li>1 M <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/normedtype.glob</code></li>
              <li>1 M <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/topology.vo</code></li>
              <li>1 M <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/topology.glob</code></li>
              <li>915 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/derive.vo</code></li>
              <li>755 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/ereal.glob</code></li>
              <li>726 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/derive.glob</code></li>
              <li>617 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/ereal.vo</code></li>
              <li>565 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/landau.vo</code></li>
              <li>503 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/measure.vo</code></li>
              <li>462 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/sequences.glob</code></li>
              <li>452 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/sequences.vo</code></li>
              <li>428 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/landau.glob</code></li>
              <li>410 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/altreals/realsum.glob</code></li>
              <li>396 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/altreals/distr.glob</code></li>
              <li>344 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/classical_sets.glob</code></li>
              <li>344 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/altreals/realsum.vo</code></li>
              <li>339 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/altreals/distr.vo</code></li>
              <li>321 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/classical_sets.vo</code></li>
              <li>226 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/Rstruct.vo</code></li>
              <li>205 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/reals.vo</code></li>
              <li>198 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/altreals/realseq.vo</code></li>
              <li>191 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/forms.vo</code></li>
              <li>181 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/measure.glob</code></li>
              <li>173 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/topology.v</code></li>
              <li>159 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/Rstruct.glob</code></li>
              <li>154 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/forms.glob</code></li>
              <li>151 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/boolp.glob</code></li>
              <li>149 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/altreals/realseq.glob</code></li>
              <li>146 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/reals.glob</code></li>
              <li>137 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/normedtype.v</code></li>
              <li>129 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/boolp.vo</code></li>
              <li>106 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/nngnum.vo</code></li>
              <li>99 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/nngnum.glob</code></li>
              <li>91 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/altreals/discrete.vo</code></li>
              <li>90 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/altreals/xfinmap.vo</code></li>
              <li>80 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/summability.vo</code></li>
              <li>72 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/ereal.v</code></li>
              <li>70 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/posnum.vo</code></li>
              <li>66 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/landau.v</code></li>
              <li>63 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/derive.v</code></li>
              <li>57 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/classical_sets.v</code></li>
              <li>52 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/sequences.v</code></li>
              <li>47 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/prodnormedzmodule.vo</code></li>
              <li>45 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/altreals/xfinmap.glob</code></li>
              <li>45 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/altreals/realsum.v</code></li>
              <li>41 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/altreals/distr.v</code></li>
              <li>34 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/posnum.glob</code></li>
              <li>33 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/altreals/discrete.glob</code></li>
              <li>29 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/measure.v</code></li>
              <li>28 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/boolp.v</code></li>
              <li>26 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/Rstruct.v</code></li>
              <li>24 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/reals.v</code></li>
              <li>23 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/forms.v</code></li>
              <li>20 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/altreals/realseq.v</code></li>
              <li>16 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/prodnormedzmodule.glob</code></li>
              <li>13 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/nngnum.v</code></li>
              <li>8 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/summability.glob</code></li>
              <li>8 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/posnum.v</code></li>
              <li>7 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/altreals/discrete.v</code></li>
              <li>5 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/altreals/xfinmap.v</code></li>
              <li>2 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/prodnormedzmodule.v</code></li>
              <li>2 K <code>../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/mathcomp/analysis/summability.v</code></li>
            </ul>
            <h2>Uninstall 🧹</h2>
            <dl class="dl-horizontal">
              <dt>Command</dt>
              <dd><code>opam remove -y coq-mathcomp-analysis.0.3.6</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>
