<!DOCTYPE html>
<html lang="en">
  <head>
    <meta charset="utf-8">
    <meta name="viewport" content="width=device-width, initial-scale=1">
    <title>monae: Black list 🏴‍☠️</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.7.1+2 / monae - 0.2.2</a></li>
            </ul>
          </div>
        </div>
      </div>
      <div class="article">
        <div class="row">
          <div class="col-md-12">
            <a href="../..">« Up</a>
            <h1>
              monae
              <small>
                0.2.2
                <span class="label label-default">Black list 🏴‍☠️</span>
              </small>
            </h1>
            <p>📅 <em><script>document.write(moment("2022-01-27 01:18:40 +0000", "YYYY-MM-DD HH:mm:ss Z").fromNow());</script> (2022-01-27 01:18:40 UTC)</em><p>
            <div class="alert alert-info" role="alert">
              <p>This result is black-listed as it is considered as too hard to reproduce / to solve. If you find a way to fix this package, please make a pull-request to <a class="alert-link" href="https://github.com/coq/opam-coq-archive">github.com/coq/opam-coq-archive</a>. The list of black-listed packages is in <a class="alert-link" href="https://github.com/coq-bench/make-html/blob/master/black_list.rb">black_list.rb</a>.</p>
            </div>
            <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.14        Preprocessor-pretty-printer of OCaml
conf-findutils      1           Virtual package relying on findutils
conf-perl           2           Virtual package relying on perl
coq                 8.7.1+2     Formal proof management system
num                 0           The Num library for arbitrary-precision integer and rational arithmetic
ocaml               4.03.0      The OCaml compiler (virtual package)
ocaml-base-compiler 4.03.0      Official 4.03.0 release
ocaml-config        1           OCaml Switch Configuration
ocamlfind           1.9.2       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/affeldt-aist/monae&quot;
dev-repo: &quot;git+https://github.com/affeldt-aist/monae.git&quot;
bug-reports: &quot;https://github.com/affeldt-aist/monae/issues&quot;
license: &quot;LGPL-2.1-or-later&quot;
synopsis: &quot;Monads and equational reasoning in Coq&quot;
description: &quot;&quot;&quot;
This Coq library contains a hierarchy of monads with their laws used
in several examples of monadic equational reasoning.&quot;&quot;&quot;
build: [
  [make &quot;-j%{jobs}%&quot;]
  [make &quot;sect5&quot;]
  [make &quot;-C&quot; &quot;impredicative_set&quot;]
]
install: [make &quot;install&quot;]
depends: [
  &quot;coq&quot; { (&gt;= &quot;8.11&quot; &amp; &lt; &quot;8.13~&quot;) | (= &quot;dev&quot;) }
  &quot;coq-mathcomp-ssreflect&quot; { (&gt;= &quot;1.11.0&quot; &amp; &lt; &quot;1.13~&quot;) }
  &quot;coq-mathcomp-fingroup&quot; { (&gt;= &quot;1.11.0&quot; &amp; &lt; &quot;1.13~&quot;) }
  &quot;coq-mathcomp-algebra&quot; { (&gt;= &quot;1.11.0&quot; &amp; &lt; &quot;1.13~&quot;) }
  &quot;coq-mathcomp-solvable&quot; { (&gt;= &quot;1.11.0&quot; &amp; &lt; &quot;1.13~&quot;) }
  &quot;coq-mathcomp-field&quot; { (&gt;= &quot;1.11.0&quot; &amp; &lt; &quot;1.13~&quot;) }
  &quot;coq-mathcomp-analysis&quot; { (&gt;= &quot;0.3.4&quot; &amp; &lt; &quot;0.3.6~&quot;) }
  &quot;coq-infotheo&quot; { &gt;= &quot;0.2.1&quot; &amp; &lt; &quot;0.3~&quot;}
  &quot;coq-paramcoq&quot; { &gt;= &quot;1.1.2&quot; &amp; &lt; &quot;1.2~&quot; }
]
tags: [
  &quot;keyword:monae&quot;
  &quot;keyword:effects&quot;
  &quot;keyword:probability&quot;
  &quot;keyword:nondeterminism&quot;
  &quot;logpath:monae&quot;
]
authors: [
  &quot;Reynald Affeldt&quot;
  &quot;David Nowak&quot;
  &quot;Takafumi Saikawa&quot;
  &quot;Jacques Garrigue&quot;
  &quot;Celestine Sauvage&quot;
  &quot;Kazunari Tanaka&quot;
]
url {
  http: &quot;https://github.com/affeldt-aist/monae/archive/0.2.2.tar.gz&quot;
  checksum: &quot;sha512=a752aa916752306c3ce5231e118d96154633976bcd1062174496c9f74b7d5f216c6d70552f1abcc1ea1b0706708938e6d6ffc8c05b276eec779c80ec90b70660&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-monae.0.2.2 coq.8.7.1+2</code></dd>
              <dt>Return code</dt>
              <dd>5120</dd>
              <dt>Output</dt>
              <dd><pre>[NOTE] Package coq is already installed (current version is 8.7.1+2).
The following dependencies couldn&#39;t be met:
  - coq-monae -&gt; coq &gt;= dev -&gt; ocaml &gt;= 4.05.0
      base of this switch (use `--unlock-base&#39; to force)
No solution found, exiting
</pre></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>opam remove -y coq; opam install -y --show-action --unlock-base coq-monae.0.2.2</code></dd>
              <dt>Return code</dt>
              <dd>15360</dd>
              <dt>Output</dt>
              <dd><pre>The following actions will be performed:
  - remove coq 8.7.1+2
&lt;&gt;&lt;&gt; Processing actions &lt;&gt;&lt;&gt;&lt;&gt;&lt;&gt;&lt;&gt;&lt;&gt;&lt;&gt;&lt;&gt;&lt;&gt;&lt;&gt;&lt;&gt;&lt;&gt;&lt;&gt;&lt;&gt;&lt;&gt;&lt;&gt;&lt;&gt;&lt;&gt;&lt;&gt;&lt;&gt;&lt;&gt;&lt;&gt;&lt;&gt;&lt;&gt;&lt;&gt;&lt;&gt;&lt;&gt;&lt;&gt;
[WARNING] package uninstall script failed at /home/bench/.opam/opam-init/hooks/sandbox.sh remove rm -R /home/bench/.opam/ocaml-base-compiler.4.03.0/lib/coq /home/bench/.opam/ocaml-base-compiler.4.03.0/share/coq:
          # context              2.0.5 | linux/x86_64 | ocaml-base-compiler.4.03.0 | https://opam.ocaml.org#d4502500
          # path                 ~/run
          # command              ~/.opam/opam-init/hooks/sandbox.sh remove rm -R /home/bench/.opam/ocaml-base-compiler.4.03.0/lib/coq /home/bench/.opam/ocaml-base-compiler.4.03.0/share/coq
          # exit-code            1
          # env-file             ~/.opam/log/coq-842-9b8556.env
          # output-file          ~/.opam/log/coq-842-9b8556.out
          ### output ###
          # rm: cannot remove &#39;/home/bench/.opam/ocaml-base-compiler.4.03.0/share/coq&#39;: No such file or directory
Done.
# Run eval $(opam env) to update the current shell environment
[ERROR] Sorry, resolution of the request timed out.
        Try to specify a simpler request, use a different solver, or increase the allowed time by setting OPAMSOLVERTIMEOUT to a bigger value (currently, it is set to 600.0 seconds).
</pre></dd>
            </dl>
            <h2>Install dependencies</h2>
            <dl class="dl-horizontal">
              <dt>Command</dt>
              <dd><code>true</code></dd>
              <dt>Return code</dt>
              <dd>0</dd>
              <dt>Duration</dt>
              <dd>0 s</dd>
            </dl>
            <h2>Install 🚀</h2>
            <dl class="dl-horizontal">
              <dt>Command</dt>
              <dd><code>true</code></dd>
              <dt>Return code</dt>
              <dd>0</dd>
              <dt>Duration</dt>
              <dd>0 s</dd>
            </dl>
            <h2>Installation size</h2>
            <p>No files were installed.</p>
            <h2>Uninstall 🧹</h2>
            <dl class="dl-horizontal">
              <dt>Command</dt>
              <dd><code>true</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>
