<!DOCTYPE html>
<html lang="en">
  <head>
    <meta charset="utf-8">
    <meta name="viewport" content="width=device-width, initial-scale=1">
    <title>buchberger: 1 m 42 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.11.1 / buchberger - 8.11.0</a></li>
            </ul>
          </div>
        </div>
      </div>
      <div class="article">
        <div class="row">
          <div class="col-md-12">
            <a href="../..">« Up</a>
            <h1>
              buchberger
              <small>
                8.11.0
                <span class="label label-success">1 m 42 s 🏆</span>
              </small>
            </h1>
            <p>📅 <em><script>document.write(moment("2022-02-19 08:01:03 +0000", "YYYY-MM-DD HH:mm:ss Z").fromNow());</script> (2022-02-19 08:01:03 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.11.1      Formal proof management system
num                 1.4         The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml               4.08.1      The OCaml compiler (virtual package)
ocaml-base-compiler 4.08.1      Official release 4.08.1
ocaml-config        1           OCaml Switch Configuration
ocamlfind           1.9.3       A library manager for OCaml
# opam file:
opam-version: &quot;2.0&quot;
maintainer: &quot;palmskog@gmail.com&quot;
homepage: &quot;https://github.com/coq-community/buchberger&quot;
dev-repo: &quot;git+https://github.com/coq-community/buchberger.git&quot;
bug-reports: &quot;https://github.com/coq-community/buchberger/issues&quot;
license: &quot;LGPL-2.1-or-later&quot;
synopsis: &quot;Verified implementation of Buchberger&#39;s algorithm for computing Gröbner bases in Coq&quot;
description: &quot;&quot;&quot;
A verified implementation of Buchberger&#39;s algorithm in Coq,
which computes the Gröbner basis associated with a polynomial ideal.
Also includes a constructive proof of Dickson&#39;s lemma.&quot;&quot;&quot;
build: [make &quot;-j%{jobs}%&quot;]
install: [make &quot;install&quot;]
depends: [
  &quot;coq&quot; {&gt;= &quot;8.7&quot; &amp; &lt; &quot;8.13~&quot;}
]
tags: [
  &quot;category:Mathematics/Algebra&quot;
  &quot;category:Miscellaneous/Extracted Programs/Combinatorics&quot;
  &quot;keyword:Gröbner basis&quot;
  &quot;keyword:polynomial ideal&quot;
  &quot;keyword:Buchberger&#39;s algorithm&quot;
  &quot;logpath:Buchberger&quot;
  &quot;date:2020-05-27&quot;
]
authors: [
  &quot;Laurent Théry&quot;
  &quot;Henrik Persson&quot;
]
url {
  src: &quot;https://github.com/coq-community/buchberger/archive/v8.11.0.tar.gz&quot;
  checksum: &quot;sha512=a048ee35574090d2ffa6b8c6a5e4379bb5f7699e0b84c1c4781fb624d151faca02eb9122bae2d21296ba6dbe57adb116edaa1255a5475b1cbafe89d33d364a05&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-buchberger.8.11.0 coq.8.11.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-buchberger.8.11.0 coq.8.11.1</code></dd>
              <dt>Return code</dt>
              <dd>0</dd>
              <dt>Duration</dt>
              <dd>13 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-buchberger.8.11.0 coq.8.11.1</code></dd>
              <dt>Return code</dt>
              <dd>0</dd>
              <dt>Duration</dt>
              <dd>1 m 42 s</dd>
            </dl>
            <h2>Installation size</h2>
            <p>Total: 8 M</p>
            <ul>
              <li>537 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Pspoly.glob</code></li>
              <li>507 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Pspminus.glob</code></li>
              <li>393 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Pcrit.glob</code></li>
              <li>388 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Preduceplus.glob</code></li>
              <li>300 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Pminus.glob</code></li>
              <li>294 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Pplus.glob</code></li>
              <li>283 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Buch.glob</code></li>
              <li>266 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/BuchRed.glob</code></li>
              <li>231 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Preduce.glob</code></li>
              <li>220 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Buch.vo</code></li>
              <li>206 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Preducestar.vo</code></li>
              <li>195 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Pcomb.glob</code></li>
              <li>176 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/BuchAux.glob</code></li>
              <li>173 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Pspoly.vo</code></li>
              <li>173 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Pminus.vo</code></li>
              <li>171 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/DivTerm.glob</code></li>
              <li>167 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Pplus.vo</code></li>
              <li>151 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Pmult.glob</code></li>
              <li>147 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Pmults.glob</code></li>
              <li>144 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/BuchAux.vo</code></li>
              <li>132 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/BuchRed.vo</code></li>
              <li>118 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Preduce.vo</code></li>
              <li>118 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Preducestar.glob</code></li>
              <li>114 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Preduceplus.vo</code></li>
              <li>110 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Pcrit.vo</code></li>
              <li>102 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/DivTerm.vo</code></li>
              <li>99 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Pcomb.vo</code></li>
              <li>95 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Pspminus.vo</code></li>
              <li>83 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/POrder.vo</code></li>
              <li>82 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Monomials.glob</code></li>
              <li>76 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Peq.vo</code></li>
              <li>74 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Term.vo</code></li>
              <li>72 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/WfR0.glob</code></li>
              <li>69 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/POrder.glob</code></li>
              <li>69 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Pspoly.v</code></li>
              <li>66 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Term.glob</code></li>
              <li>65 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Pmults.vo</code></li>
              <li>61 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Pspminus.v</code></li>
              <li>60 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Monomials.vo</code></li>
              <li>57 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Relation_Operators_compat.glob</code></li>
              <li>56 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Pmult.vo</code></li>
              <li>51 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Pcrit.v</code></li>
              <li>51 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Relation_Operators_compat.vo</code></li>
              <li>48 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/WfR0.vo</code></li>
              <li>47 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/moreCoefStructure.glob</code></li>
              <li>46 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Preduceplus.v</code></li>
              <li>46 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Dickson.vo</code></li>
              <li>46 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Pplus.v</code></li>
              <li>45 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Buch.v</code></li>
              <li>44 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Pminus.v</code></li>
              <li>39 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Peq.glob</code></li>
              <li>39 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Bar.vo</code></li>
              <li>35 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Fred.glob</code></li>
              <li>34 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Fred.vo</code></li>
              <li>33 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/BuchRed.v</code></li>
              <li>32 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Preduce.v</code></li>
              <li>30 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/LexiOrder.vo</code></li>
              <li>30 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/DivTerm.v</code></li>
              <li>27 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/CoefStructure.vo</code></li>
              <li>27 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Pcomb.v</code></li>
              <li>25 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Dickson.glob</code></li>
              <li>24 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/BuchAux.v</code></li>
              <li>21 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Pmults.v</code></li>
              <li>20 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Pmult.v</code></li>
              <li>19 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/moreCoefStructure.vo</code></li>
              <li>19 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Bar.glob</code></li>
              <li>17 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Term.v</code></li>
              <li>16 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/POrder.v</code></li>
              <li>15 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/ListProps.vo</code></li>
              <li>14 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Preducestar.v</code></li>
              <li>14 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/OpenIndGoodRel.vo</code></li>
              <li>13 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Monomials.v</code></li>
              <li>13 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/CoefStructure.glob</code></li>
              <li>10 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Relation_Operators_compat.v</code></li>
              <li>9 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Fred.v</code></li>
              <li>9 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Peq.v</code></li>
              <li>8 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/LexiOrder.glob</code></li>
              <li>6 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/OrderStructure.vo</code></li>
              <li>6 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/moreCoefStructure.v</code></li>
              <li>6 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/WfR0.v</code></li>
              <li>6 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Dickson.v</code></li>
              <li>5 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/Bar.v</code></li>
              <li>4 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/ListProps.glob</code></li>
              <li>4 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/OpenIndGoodRel.glob</code></li>
              <li>3 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/LexiOrder.v</code></li>
              <li>3 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/OrderStructure.glob</code></li>
              <li>2 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/CoefStructure.v</code></li>
              <li>2 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/LetP.vo</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/ListProps.v</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/LetP.v</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/OpenIndGoodRel.v</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/OrderStructure.v</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Buchberger/LetP.glob</code></li>
            </ul>
            <h2>Uninstall 🧹</h2>
            <dl class="dl-horizontal">
              <dt>Command</dt>
              <dd><code>opam remove -y coq-buchberger.8.11.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">
          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>
