<!DOCTYPE html>
<html lang="en">
  <head>
    <meta charset="utf-8">
    <meta name="viewport" content="width=device-width, initial-scale=1">
    <title>monae: 5 m 47 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.2 / monae - 0.1.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.1.2
                <span class="label label-success">5 m 47 s</span>
              </small>
            </h1>
            <p><em><script>document.write(moment("2020-08-17 11:46:38 +0000", "YYYY-MM-DD HH:mm:ss Z").fromNow());</script> (2020-08-17 11:46:38 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
conf-m4             1           Virtual package relying on m4
coq                 8.11.2      Formal proof management system
num                 1.3         The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml               4.10.0      The OCaml compiler (virtual package)
ocaml-base-compiler 4.10.0      Official release 4.10.0
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;reynald.affeldt@aist.go.jp&quot;
homepage: &quot;https://github.com/affeldt-aist/monae&quot;
bug-reports: &quot;https://github.com/affeldt-aist/monae/issues&quot;
dev-repo: &quot;git+https://github.com/affeldt-aist/monae.git&quot;
license: &quot;GPL-3.0-or-later&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;
]
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;coq-infotheo&quot; { &gt;= &quot;0.1.2&quot; &amp; &lt; &quot;0.2~&quot; }
  &quot;coq-paramcoq&quot; { &gt;= &quot;1.1.2&quot; &amp; &lt; &quot;1.2~&quot; }
]
synopsis: &quot;Monae&quot;
description: &quot;&quot;&quot;
This repository contains a formalization of monads including several
models, examples of monadic equational reasoning, and an application
to program semantics.
&quot;&quot;&quot;
tags: [
  &quot;category:Computer Science/Semantics&quot;
  &quot;keyword: monad&quot;
  &quot;keyword: effect&quot;
  &quot;keyword: probability&quot;
  &quot;keyword: nondeterminism&quot;
  &quot;logpath:monae&quot;
  &quot;date:2020-08-13&quot;
]
url {
  http: &quot;https://github.com/affeldt-aist/monae/archive/0.1.2.tar.gz&quot;
  checksum: &quot;sha512=fc06a3dc53e180940478ca8ec02755432c1fb29b6ed81f3312731a1d0435dbe67e78db5201a92e40c7f23068fc5d9343414fc06676bf3adf402836e8c69b0229&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.1.2 coq.8.11.2</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-monae.0.1.2 coq.8.11.2</code></dd>
              <dt>Return code</dt>
              <dd>0</dd>
              <dt>Duration</dt>
              <dd>51 m 4 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-monae.0.1.2 coq.8.11.2</code></dd>
              <dt>Return code</dt>
              <dd>0</dd>
              <dt>Duration</dt>
              <dd>5 m 47 s</dd>
            </dl>
            <h2>Installation size</h2>
            <p>Total: 9 M</p>
            <ul>
              <li>1 M <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/category.vo</code></li>
              <li>898 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/monad_transformer.vo</code></li>
              <li>504 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/hierarchy.vo</code></li>
              <li>457 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/smallstep.vo</code></li>
              <li>402 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/monad_model.vo</code></li>
              <li>315 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/state_lib.vo</code></li>
              <li>308 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/monad_transformer.glob</code></li>
              <li>286 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/hierarchy.glob</code></li>
              <li>275 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/example_monty.glob</code></li>
              <li>270 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/category.glob</code></li>
              <li>255 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/fail_lib.vo</code></li>
              <li>255 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/example_monty.vo</code></li>
              <li>241 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/gcm_model.vo</code></li>
              <li>227 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/monad_model.glob</code></li>
              <li>192 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/example_nqueens.vo</code></li>
              <li>189 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/altprob_model.vo</code></li>
              <li>182 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/state_lib.glob</code></li>
              <li>179 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/proba_lib.vo</code></li>
              <li>178 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/monad_lib.vo</code></li>
              <li>160 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/monad_composition.vo</code></li>
              <li>157 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/example_nqueens.glob</code></li>
              <li>152 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/fail_lib.glob</code></li>
              <li>139 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/smallstep.glob</code></li>
              <li>138 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/proba_lib.glob</code></li>
              <li>124 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/gcm_model.glob</code></li>
              <li>120 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/example_relabeling.vo</code></li>
              <li>113 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/monad_lib.glob</code></li>
              <li>112 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/example_spark.vo</code></li>
              <li>99 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/example_spark.glob</code></li>
              <li>96 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/trace_lib.vo</code></li>
              <li>93 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/monad_composition.glob</code></li>
              <li>81 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/proba_monad_model.vo</code></li>
              <li>81 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/altprob_model.glob</code></li>
              <li>73 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/example_relabeling.glob</code></li>
              <li>60 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/hierarchy.v</code></li>
              <li>50 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/monae_lib.vo</code></li>
              <li>49 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/monad_transformer.v</code></li>
              <li>47 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/monad_model.v</code></li>
              <li>42 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/category.v</code></li>
              <li>29 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/smallstep.v</code></li>
              <li>28 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/gcm_model.v</code></li>
              <li>23 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/fail_lib.v</code></li>
              <li>23 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/trace_lib.glob</code></li>
              <li>23 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/example_monty.v</code></li>
              <li>22 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/state_lib.v</code></li>
              <li>19 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/monad_lib.v</code></li>
              <li>18 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/example_nqueens.v</code></li>
              <li>17 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/monae_lib.glob</code></li>
              <li>14 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/proba_lib.v</code></li>
              <li>14 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/altprob_model.v</code></li>
              <li>11 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/proba_monad_model.glob</code></li>
              <li>10 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/monad_composition.v</code></li>
              <li>10 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/example_spark.v</code></li>
              <li>7 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/example_relabeling.v</code></li>
              <li>4 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/monae_lib.v</code></li>
              <li>4 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/trace_lib.v</code></li>
              <li>3 K <code>../ocaml-base-compiler.4.10.0/lib/coq/user-contrib/monae/proba_monad_model.v</code></li>
            </ul>
            <h2>Uninstall</h2>
            <dl class="dl-horizontal">
              <dt>Command</dt>
              <dd><code>opam remove -y coq-monae.0.1.2</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>
