<!DOCTYPE html>
<html lang="en">
  <head>
    <meta charset="utf-8">
    <meta name="viewport" content="width=device-width, initial-scale=1">
    <title>metacoq-erasure: 3 m 5 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.9.0 / metacoq-erasure - 1.0~alpha+8.9</a></li>
            </ul>
          </div>
        </div>
      </div>
      <div class="article">
        <div class="row">
          <div class="col-md-12">
            <a href="../..">« Up</a>
            <h1>
              metacoq-erasure
              <small>
                1.0~alpha+8.9
                <span class="label label-success">3 m 5 s</span>
              </small>
            </h1>
            <p><em><script>document.write(moment("2020-07-26 11:43:01 +0000", "YYYY-MM-DD HH:mm:ss Z").fromNow());</script> (2020-07-26 11:43:01 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
camlp5              7.12        Preprocessor-pretty-printer of OCaml
conf-findutils      1           Virtual package relying on findutils
conf-m4             1           Virtual package relying on m4
coq                 8.9.0       Formal proof management system
num                 0           The Num library for arbitrary-precision integer and rational arithmetic
ocaml               4.04.2      The OCaml compiler (virtual package)
ocaml-base-compiler 4.04.2      Official 4.04.2 release
ocaml-config        1           OCaml Switch Configuration
ocamlfind           1.8.1       A library manager for OCaml
# opam file:
opam-version: &quot;2.0&quot;
maintainer: &quot;matthieu.sozeau@inria.fr&quot;
homepage: &quot;https://metacoq.github.io/metacoq&quot;
dev-repo: &quot;git+https://github.com/MetaCoq/metacoq.git#coq-8.8&quot;
bug-reports: &quot;https://github.com/MetaCoq/metacoq/issues&quot;
authors: [&quot;Abhishek Anand &lt;aa755@cs.cornell.edu&gt;&quot;
          &quot;Simon Boulier &lt;simon.boulier@inria.fr&gt;&quot;
          &quot;Cyril Cohen &lt;cyril.cohen@inria.fr&gt;&quot;
          &quot;Yannick Forster &lt;forster@ps.uni-saarland.de&gt;&quot;
          &quot;Fabian Kunze &lt;fkunze@fakusb.de&gt;&quot;
          &quot;Gregory Malecha &lt;gmalecha@gmail.com&gt;&quot;
          &quot;Matthieu Sozeau &lt;matthieu.sozeau@inria.fr&gt;&quot;
          &quot;Nicolas Tabareau &lt;nicolas.tabareau@inria.fr&gt;&quot;
          &quot;Théo Winterhalter &lt;theo.winterhalter@inria.fr&gt;&quot;
]
license: &quot;MIT&quot;
build: [
  [&quot;sh&quot; &quot;./configure.sh&quot;]
  [make &quot;-j%{jobs}%&quot; &quot;-C&quot; &quot;erasure&quot;]
  [make &quot;test-suite&quot;] {with-test}
]
install: [
  [make &quot;-C&quot; &quot;erasure&quot; &quot;install&quot;]
]
depends: [
  &quot;ocaml&quot; {&gt; &quot;4.02.3&quot;}
  &quot;coq&quot; {&gt;= &quot;8.9&quot; &amp; &lt; &quot;8.10~&quot;}
  &quot;coq-metacoq-template&quot; {= version}
  &quot;coq-metacoq-checker&quot; {= version}
  &quot;coq-metacoq-pcuic&quot; {= version}
  &quot;coq-metacoq-safechecker&quot; {= version}
]
synopsis: &quot;Implementation and verification of an erasure procedure for Coq&quot;
description: &quot;&quot;&quot;
MetaCoq is a meta-programming framework for Coq.
The Erasure module provides a complete specification of Coq&#39;s so-called
\&quot;extraction\&quot; procedure, starting from the PCUIC calculus and targeting
untyped call-by-value lambda-calculus.
The `erasure` function translates types and proofs in well-typed terms
into a dummy `tBox` constructor, following closely P. Letouzey&#39;s PhD
thesis.
&quot;&quot;&quot;
url {
  src: &quot;https://github.com/MetaCoq/metacoq/archive/1.0-alpha+8.9.tar.gz&quot;
  checksum: &quot;sha256=899ef4ee73b1684a0f1d2e37ab9ab0f9b24424f6d8a10a10efd474c0ed93488e&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-metacoq-erasure.1.0~alpha+8.9 coq.8.9.0</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-metacoq-erasure.1.0~alpha+8.9 coq.8.9.0</code></dd>
              <dt>Return code</dt>
              <dd>0</dd>
              <dt>Duration</dt>
              <dd>25 m 27 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-metacoq-erasure.1.0~alpha+8.9 coq.8.9.0</code></dd>
              <dt>Return code</dt>
              <dd>0</dd>
              <dt>Duration</dt>
              <dd>3 m 5 s</dd>
            </dl>
            <h2>Installation size</h2>
            <p>Total: 13 M</p>
            <ul>
              <li>3 M <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/ErasureFunction.vo</code></li>
              <li>1 M <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/ErasureCorrectness.vo</code></li>
              <li>1 M <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/SafeErasureFunction.vo</code></li>
              <li>980 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/ESubstitution.vo</code></li>
              <li>897 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/metacoq_erasure_plugin.cmxs</code></li>
              <li>866 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/SafeTemplateErasure.vo</code></li>
              <li>824 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/Prelim.vo</code></li>
              <li>794 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/EArities.vo</code></li>
              <li>793 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/Extraction.vo</code></li>
              <li>756 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/EInversion.vo</code></li>
              <li>364 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/ELiftSubst.vo</code></li>
              <li>177 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/metacoq_erasure_plugin.cmi</code></li>
              <li>172 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/Extract.vo</code></li>
              <li>158 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/ErasureCorrectness.glob</code></li>
              <li>123 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/ELiftSubst.glob</code></li>
              <li>114 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/EAll.vo</code></li>
              <li>114 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/EWcbvEval.vo</code></li>
              <li>108 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/ErasureFunction.glob</code></li>
              <li>97 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/EAstUtils.vo</code></li>
              <li>79 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/EArities.glob</code></li>
              <li>77 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/SafeErasureFunction.glob</code></li>
              <li>70 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/metacoq_erasure_plugin.cmx</code></li>
              <li>68 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/EWcbvEval.glob</code></li>
              <li>66 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/ESubstitution.glob</code></li>
              <li>63 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/EAst.vo</code></li>
              <li>63 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/EPretty.vo</code></li>
              <li>53 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/ETyping.vo</code></li>
              <li>49 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/Prelim.glob</code></li>
              <li>49 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/ErasureCorrectness.v</code></li>
              <li>42 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/EInduction.vo</code></li>
              <li>38 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/Extract.glob</code></li>
              <li>37 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/EAstUtils.glob</code></li>
              <li>36 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/EWndEval.vo</code></li>
              <li>34 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/Loader.vo</code></li>
              <li>30 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/ErasureFunction.v</code></li>
              <li>26 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/SafeErasureFunction.v</code></li>
              <li>26 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/SafeTemplateErasure.glob</code></li>
              <li>26 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/EPretty.glob</code></li>
              <li>23 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/EWcbvEval.v</code></li>
              <li>22 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/EArities.v</code></li>
              <li>22 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/EInversion.glob</code></li>
              <li>17 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/ELiftSubst.v</code></li>
              <li>15 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/ESubstitution.v</code></li>
              <li>13 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/EAst.glob</code></li>
              <li>12 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/Prelim.v</code></li>
              <li>11 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/ETyping.glob</code></li>
              <li>9 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/SafeTemplateErasure.v</code></li>
              <li>8 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/EAstUtils.v</code></li>
              <li>8 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/EInduction.glob</code></li>
              <li>7 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/Extract.v</code></li>
              <li>6 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/EPretty.v</code></li>
              <li>6 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/metacoq_erasure_plugin.cmxa</code></li>
              <li>6 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/EAst.v</code></li>
              <li>3 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/ETyping.v</code></li>
              <li>3 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/EWndEval.v</code></li>
              <li>3 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/EInversion.v</code></li>
              <li>3 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/EInduction.v</code></li>
              <li>2 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/EWndEval.glob</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/Extraction.v</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/Extraction.glob</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/EAll.glob</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/Loader.glob</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/Loader.v</code></li>
              <li>1 K <code>../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/MetaCoq/Erasure/EAll.v</code></li>
            </ul>
            <h2>Uninstall</h2>
            <dl class="dl-horizontal">
              <dt>Command</dt>
              <dd><code>opam remove -y coq-metacoq-erasure.1.0~alpha+8.9</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>
