<!DOCTYPE html>
<html lang="en">
  <head>
    <meta charset="utf-8">
    <meta name="viewport" content="width=device-width, initial-scale=1">
    <title>mathcomp-solvable: 8 m 9 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.5.0~camlp4 / mathcomp-solvable - 1.6.1</a></li>
            </ul>
          </div>
        </div>
      </div>
      <div class="article">
        <div class="row">
          <div class="col-md-12">
            <a href="../..">« Up</a>
            <h1>
              mathcomp-solvable
              <small>
                1.6.1
                <span class="label label-success">8 m 9 s</span>
              </small>
            </h1>
            <p><em><script>document.write(moment("2020-09-09 03:51:12 +0000", "YYYY-MM-DD HH:mm:ss Z").fromNow());</script> (2020-09-09 03:51:12 UTC)</em><p>
            <h2>Context</h2>
            <pre># Packages matching: installed
# Name              # Installed  # Synopsis
base-bigarray       base
base-num            base         Num library distributed with the OCaml compiler
base-threads        base
base-unix           base
camlp4              4.05+1       Camlp4 is a system for writing extensible parsers for programming languages
conf-findutils      1            Virtual package relying on findutils
coq                 8.5.0~camlp4 Formal proof management system.
num                 0            The Num library for arbitrary-precision integer and rational arithmetic
ocaml               4.05.0       The OCaml compiler (virtual package)
ocaml-base-compiler 4.05.0       Official 4.05.0 release
ocaml-config        1            OCaml Switch Configuration
ocamlbuild          0.14.0       OCamlbuild is a build system with builtin rules to easily build most OCaml projects.
# opam file:
opam-version: &quot;2.0&quot;
name: &quot;coq-mathcomp-solvable&quot;
version: &quot;1.6.1&quot;
maintainer: &quot;Mathematical Components &lt;mathcomp-dev@sympa.inria.fr&gt;&quot;
homepage: &quot;http://ssr.msr-inria.inria.fr/&quot;
bug-reports: &quot;Mathematical Components &lt;mathcomp-dev@sympa.inria.fr&gt;&quot;
license: &quot;CeCILL-B&quot;
build: [ make &quot;-C&quot; &quot;mathcomp/solvable&quot; &quot;-j&quot; &quot;%{jobs}%&quot; ]
install: [ make &quot;-C&quot; &quot;mathcomp/solvable&quot; &quot;install&quot; ]
remove: [ &quot;sh&quot; &quot;-c&quot; &quot;rm -rf &#39;%{lib}%/coq/user-contrib/mathcomp/solvable&#39;&quot; ]
depends: [
  &quot;ocaml&quot;
  &quot;coq-mathcomp-algebra&quot; {= &quot;1.6.1&quot;}
]
tags: [ &quot;keyword:finite groups&quot; &quot;keyword:Feit Thompson theorem&quot; &quot;keyword:small scale reflection&quot; &quot;keyword:mathematical components&quot; &quot;keyword:odd order theorem&quot; ]
authors: [ &quot;Jeremy Avigad &lt;&gt;&quot; &quot;Andrea Asperti &lt;&gt;&quot; &quot;Stephane Le Roux &lt;&gt;&quot; &quot;Yves Bertot &lt;&gt;&quot; &quot;Laurence Rideau &lt;&gt;&quot; &quot;Enrico Tassi &lt;&gt;&quot; &quot;Ioana Pasca &lt;&gt;&quot; &quot;Georges Gonthier &lt;&gt;&quot; &quot;Sidi Ould Biha &lt;&gt;&quot; &quot;Cyril Cohen &lt;&gt;&quot; &quot;Francois Garillot &lt;&gt;&quot; &quot;Alexey Solovyev &lt;&gt;&quot; &quot;Russell O&#39;Connor &lt;&gt;&quot; &quot;Laurent Théry &lt;&gt;&quot; &quot;Assia Mahboubi &lt;&gt;&quot; ]
synopsis: &quot;Mathematical Components Library on finite groups (II)&quot;
description:
  &quot;This library contains more definitions and theorems about finite groups.&quot;
url {
  src: &quot;http://github.com/math-comp/math-comp/archive/mathcomp-1.6.1.tar.gz&quot;
  checksum: &quot;md5=10d8a17134ddb509b4afa8d3243ee1a0&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-solvable.1.6.1 coq.8.5.0~camlp4</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-mathcomp-solvable.1.6.1 coq.8.5.0~camlp4</code></dd>
              <dt>Return code</dt>
              <dd>0</dd>
              <dt>Duration</dt>
              <dd>11 m 47 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-mathcomp-solvable.1.6.1 coq.8.5.0~camlp4</code></dd>
              <dt>Return code</dt>
              <dd>0</dd>
              <dt>Duration</dt>
              <dd>8 m 9 s</dd>
            </dl>
            <h2>Installation size</h2>
            <p>Total: 16 M</p>
            <ul>
              <li>2 M <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/extremal.vo</code></li>
              <li>1 M <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/extremal.glob</code></li>
              <li>928 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/abelian.vo</code></li>
              <li>873 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/maximal.vo</code></li>
              <li>832 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/abelian.glob</code></li>
              <li>772 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/maximal.glob</code></li>
              <li>526 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/extraspecial.vo</code></li>
              <li>473 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/pgroup.glob</code></li>
              <li>447 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/hall.vo</code></li>
              <li>439 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/hall.glob</code></li>
              <li>419 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/center.vo</code></li>
              <li>408 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/extraspecial.glob</code></li>
              <li>362 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/frobenius.vo</code></li>
              <li>357 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/pgroup.vo</code></li>
              <li>329 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/finmodule.vo</code></li>
              <li>304 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/frobenius.glob</code></li>
              <li>299 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/cyclic.glob</code></li>
              <li>297 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/cyclic.vo</code></li>
              <li>297 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/alt.vo</code></li>
              <li>285 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/sylow.glob</code></li>
              <li>283 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/sylow.vo</code></li>
              <li>278 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/nilpotent.glob</code></li>
              <li>271 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/finmodule.glob</code></li>
              <li>250 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/nilpotent.vo</code></li>
              <li>247 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/jordanholder.vo</code></li>
              <li>235 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/alt.glob</code></li>
              <li>221 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/jordanholder.glob</code></li>
              <li>218 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/center.glob</code></li>
              <li>216 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/gseries.vo</code></li>
              <li>194 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/primitive_action.vo</code></li>
              <li>166 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/commutator.glob</code></li>
              <li>141 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/gseries.glob</code></li>
              <li>137 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/commutator.vo</code></li>
              <li>128 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/gfunctor.vo</code></li>
              <li>127 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/primitive_action.glob</code></li>
              <li>120 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/extremal.v</code></li>
              <li>94 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/gfunctor.glob</code></li>
              <li>88 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/abelian.v</code></li>
              <li>73 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/maximal.v</code></li>
              <li>50 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/pgroup.v</code></li>
              <li>42 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/hall.v</code></li>
              <li>41 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/extraspecial.v</code></li>
              <li>35 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/frobenius.v</code></li>
              <li>33 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/cyclic.v</code></li>
              <li>32 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/all_solvable.vo</code></li>
              <li>29 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/jordanholder.v</code></li>
              <li>28 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/nilpotent.v</code></li>
              <li>27 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/sylow.v</code></li>
              <li>27 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/finmodule.v</code></li>
              <li>24 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/center.v</code></li>
              <li>24 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/alt.v</code></li>
              <li>21 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/gseries.v</code></li>
              <li>20 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/gfunctor.v</code></li>
              <li>15 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/primitive_action.v</code></li>
              <li>13 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/commutator.v</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/all_solvable.glob</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/mathcomp/solvable/all_solvable.v</code></li>
            </ul>
            <h2>Uninstall</h2>
            <dl class="dl-horizontal">
              <dt>Command</dt>
              <dd><code>opam remove -y coq-mathcomp-solvable.1.6.1</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>
