<!DOCTYPE html>
<html lang="en">
  <head>
    <meta charset="utf-8">
    <meta name="viewport" content="width=device-width, initial-scale=1">
    <title>bignums: 2 m 32 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 / bignums - 8.12.0</a></li>
            </ul>
          </div>
        </div>
      </div>
      <div class="article">
        <div class="row">
          <div class="col-md-12">
            <a href="../..">« Up</a>
            <h1>
              bignums
              <small>
                8.12.0
                <span class="label label-success">2 m 32 s</span>
              </small>
            </h1>
            <p><em><script>document.write(moment("2021-04-16 14:57:06 +0000", "YYYY-MM-DD HH:mm:ss Z").fromNow());</script> (2021-04-16 14:57:06 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.1      The OCaml compiler (virtual package)
ocaml-base-compiler 4.10.1      Official release 4.10.1
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;Vincent.Laporte@inria.fr&quot;
homepage: &quot;https://github.com/coq/bignums&quot;
dev-repo: &quot;git+https://github.com/coq/bignums.git&quot;
bug-reports: &quot;https://github.com/coq/bignums/issues&quot;
authors: [
  &quot;Laurent Théry&quot;
  &quot;Benjamin Grégoire&quot;
  &quot;Arnaud Spiwack&quot;
  &quot;Evgeny Makarov&quot;
  &quot;Pierre Letouzey&quot;
]
license: &quot;LGPL-2.1-only&quot;
build: [
  [make &quot;-j%{jobs}%&quot; {ocaml:version &gt;= &quot;4.06&quot;}]
]
install: [
  [make &quot;install&quot;]
]
depends: [
  &quot;ocaml&quot;
  &quot;ocamlfind&quot; {build}
  &quot;coq&quot; {&gt;= &quot;8.12&quot; &amp; &lt; &quot;8.13~&quot;}
]
tags: [
  &quot;keyword:integer numbers&quot;
  &quot;keyword:rational numbers&quot;
  &quot;keyword:arithmetic&quot;
  &quot;keyword:arbitrary-precision&quot;
  &quot;category:Miscellaneous/Coq Extensions&quot;
  &quot;category:Mathematics/Arithmetic and Number Theory/Number theory&quot;
  &quot;category:Mathematics/Arithmetic and Number Theory/Rational numbers&quot;
  &quot;logpath:Bignums&quot;
]
synopsis: &quot;Bignums, the Coq library of arbitrary large numbers&quot;
description:
  &quot;Provides BigN, BigZ, BigQ that used to be part of Coq standard library &lt; 8.7.&quot;
url {
  src: &quot;https://github.com/coq/bignums/archive/V8.12.0.tar.gz&quot;
  checksum: &quot;sha512=8bec000c7b2c0e36e3a51c630132dd8e412c208a3ada22a4ae2aba6300f80ab9550b50803af901819c1ada72a0f77f5555a57fd9448d7ba734092d9fbb32d677&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-bignums.8.12.0 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 2h opam install -y --deps-only coq-bignums.8.12.0 coq.8.12.1</code></dd>
              <dt>Return code</dt>
              <dd>0</dd>
              <dt>Duration</dt>
              <dd>8 s</dd>
            </dl>
            <h2>Install</h2>
            <dl class="dl-horizontal">
              <dt>Command</dt>
              <dd><code>opam list; echo; ulimit -Sv 16000000; timeout 2h opam install -y -v coq-bignums.8.12.0 coq.8.12.1</code></dd>
              <dt>Return code</dt>
              <dd>0</dd>
              <dt>Duration</dt>
              <dd>2 m 32 s</dd>
            </dl>
            <h2>Installation size</h2>
            <p>Total: 8 M</p>
            <ul>
              <li>908 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/BigN/BigN.vo</code></li>
              <li>562 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleDiv.glob</code></li>
              <li>535 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/BigZ/BigZ.vo</code></li>
              <li>514 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/BigN/NMake.vo</code></li>
              <li>344 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleCyclic.vo</code></li>
              <li>344 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleSqrt.glob</code></li>
              <li>312 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleDiv.vo</code></li>
              <li>279 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/BigN/NMake.glob</code></li>
              <li>278 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/BigN/NMake_gen.vo</code></li>
              <li>264 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/BigQ/QMake.vo</code></li>
              <li>208 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/BigN/NMake_gen.glob</code></li>
              <li>207 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleSqrt.vo</code></li>
              <li>204 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleDivn1.glob</code></li>
              <li>201 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleCyclic.glob</code></li>
              <li>187 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleMul.glob</code></li>
              <li>179 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/SpecViaZ/ZSigZAxioms.vo</code></li>
              <li>172 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/SpecViaZ/NSigNAxioms.vo</code></li>
              <li>169 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/BigZ/ZMake.vo</code></li>
              <li>165 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/BigQ/BigQ.vo</code></li>
              <li>154 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleLift.glob</code></li>
              <li>151 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/BigQ/QMake.glob</code></li>
              <li>149 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleMul.vo</code></li>
              <li>125 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleDivn1.vo</code></li>
              <li>124 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/SpecViaQ/QSig.vo</code></li>
              <li>121 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/BigZ/ZMake.glob</code></li>
              <li>109 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleLift.vo</code></li>
              <li>96 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/BigN/Nbasic.vo</code></li>
              <li>89 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleSub.glob</code></li>
              <li>86 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleSub.vo</code></li>
              <li>78 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleBase.vo</code></li>
              <li>78 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/BigNumPrelude.vo</code></li>
              <li>76 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleAdd.vo</code></li>
              <li>76 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleBase.glob</code></li>
              <li>74 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/BigN/Nbasic.glob</code></li>
              <li>73 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleAdd.glob</code></li>
              <li>66 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/SpecViaZ/NSigNAxioms.glob</code></li>
              <li>66 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/SpecViaZ/ZSigZAxioms.glob</code></li>
              <li>64 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/BigNumPrelude.glob</code></li>
              <li>62 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/plugin/bignums_syntax_plugin.cmxs</code></li>
              <li>56 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/SpecViaZ/ZSig.vo</code></li>
              <li>55 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleDiv.v</code></li>
              <li>52 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/SpecViaZ/NSig.vo</code></li>
              <li>52 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/BigN/NMake.v</code></li>
              <li>44 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleSqrt.v</code></li>
              <li>40 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/SpecViaQ/QSig.glob</code></li>
              <li>37 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/SpecViaZ/ZSig.glob</code></li>
              <li>35 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/BigQ/QMake.v</code></li>
              <li>33 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/SpecViaZ/NSig.glob</code></li>
              <li>33 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/BigN/NMake_gen.v</code></li>
              <li>28 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleCyclic.v</code></li>
              <li>24 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleMul.v</code></li>
              <li>21 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/BigZ/ZMake.v</code></li>
              <li>20 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleDivn1.v</code></li>
              <li>19 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleLift.v</code></li>
              <li>16 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/BigZ/BigZ.glob</code></li>
              <li>16 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/BigN/Nbasic.v</code></li>
              <li>14 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/BigN/BigN.glob</code></li>
              <li>13 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleBase.v</code></li>
              <li>13 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/BigQ/BigQ.glob</code></li>
              <li>12 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleSub.v</code></li>
              <li>12 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/SpecViaZ/ZSigZAxioms.v</code></li>
              <li>11 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/SpecViaZ/NSigNAxioms.v</code></li>
              <li>11 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleAdd.v</code></li>
              <li>11 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/BigNumPrelude.v</code></li>
              <li>9 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/plugin/bignums_syntax_plugin.cmi</code></li>
              <li>8 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/plugin/bignums_syntax_plugin.cmx</code></li>
              <li>7 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/SpecViaQ/QSig.v</code></li>
              <li>6 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/BigZ/BigZ.v</code></li>
              <li>6 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/BigN/BigN.v</code></li>
              <li>5 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/BigQ/BigQ.v</code></li>
              <li>5 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/SpecViaZ/ZSig.v</code></li>
              <li>5 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/SpecViaZ/NSig.v</code></li>
              <li>4 K <code>../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/plugin/bignums_syntax_plugin.cmxa</code></li>
            </ul>
            <h2>Uninstall</h2>
            <dl class="dl-horizontal">
              <dt>Command</dt>
              <dd><code>opam remove -y coq-bignums.8.12.0</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">
          <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>
