<!DOCTYPE html>
<html lang="en">
  <head>
    <meta charset="utf-8">
    <meta name="viewport" content="width=device-width, initial-scale=1">
    <title>compcert: Not compatible</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 / extra-dev</a></li>
              <li class="active"><a href="">dev / compcert - 3.7+8.12~coq_platform</a></li>
            </ul>
          </div>
        </div>
      </div>
      <div class="article">
        <div class="row">
          <div class="col-md-12">
            <a href="../..">« Up</a>
            <h1>
              compcert
              <small>
                3.7+8.12~coq_platform
                <span class="label label-info">Not compatible</span>
              </small>
            </h1>
            <p><em><script>document.write(moment("2021-04-03 04:38:32 +0000", "YYYY-MM-DD HH:mm:ss Z").fromNow());</script> (2021-04-03 04:38:32 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-gmp            3           Virtual package relying on a GMP lib system installation
coq                 dev         Formal proof management system
num                 1.4         The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml               4.11.1      The OCaml compiler (virtual package)
ocaml-base-compiler 4.11.1      Official release 4.11.1
ocaml-config        1           OCaml Switch Configuration
ocamlfind           1.9.1       A library manager for OCaml
zarith              1.12        Implements arithmetic and logical operations over arbitrary-precision integers
# opam file:
opam-version: &quot;2.0&quot;
authors: &quot;Xavier Leroy &lt;xavier.leroy@inria.fr&gt;&quot;
maintainer: &quot;Jacques-Henri Jourdan &lt;jacques-Henri.jourdan@normalesup.org&gt;&quot;
homepage: &quot;http://compcert.inria.fr/&quot;
dev-repo: &quot;git+https://github.com/AbsInt/CompCert.git&quot;
bug-reports: &quot;https://github.com/AbsInt/CompCert/issues&quot;
license: &quot;INRIA Non-Commercial License Agreement&quot;
version: &quot;3.7&quot;
build: [
  [&quot;./configure&quot;
  &quot;ia32-linux&quot; {os = &quot;linux&quot;}
  &quot;ia32-macosx&quot; {os = &quot;macos&quot;}
  &quot;ia32-cygwin&quot; {os = &quot;cygwin&quot;}
  &quot;ia32-cygwin&quot; {os = &quot;win32&quot;}
  &quot;-bindir&quot; &quot;%{bin}%&quot;
  &quot;-libdir&quot; &quot;%{lib}%/compcert&quot;
  &quot;-install-coqdev&quot;
  &quot;-clightgen&quot;
  &quot;-coqdevdir&quot; &quot;%{lib}%/coq/user-contrib/compcert&quot;
  &quot;-ignore-coq-version&quot;]
  [make &quot;-j%{jobs}%&quot; {ocaml:version &gt;= &quot;4.06&quot;}]
]
patches: [
  &quot;0001-Install-compcert.config-file-along-the-Coq-developme.patch&quot;
  &quot;0002-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch&quot;
  &quot;0003-Update-the-list-of-dual-licensed-files.patch&quot;
  &quot;0004-Use-Coq-platform-supplied-Flocq.patch&quot;
  &quot;0005-Import-ListNotations-explicitly.patch&quot;
  &quot;0006-Coq-MenhirLib-explicit-import-ListNotations-354.patch&quot;
  &quot;0007-Use-ocamlfind-to-find-menhirLib.patch&quot;
  &quot;0008-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch&quot;
  &quot;0009-Don-t-build-MenhirLib-platform-version-is-used.patch&quot;
]
extra-files: [
  [&quot;0001-Install-compcert.config-file-along-the-Coq-developme.patch&quot; &quot;sha256=62e36964ed3d06a213caea8639be51641c25df3c4ea384e01ce57d015de698d3&quot;]
  [&quot;0002-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch&quot; &quot;sha256=1af58e827aa24be60e115878b9f70f1bf715f83bb1b91da8e2a9d749f4195d29&quot;]
  [&quot;0003-Update-the-list-of-dual-licensed-files.patch&quot; &quot;sha256=bf91c7d3e2177620296838658cafbeffdd50d8d1ef56649b56a35644410e1337&quot;]
  [&quot;0004-Use-Coq-platform-supplied-Flocq.patch&quot; &quot;sha256=83261a1fae459c319c0288a543787d3abcadaa2cccb1c34543c9784fe645f942&quot;]
  [&quot;0005-Import-ListNotations-explicitly.patch&quot; &quot;sha256=c4f29203e8dcaa17c76543ad77dabefdb555588567d4f6055cd53e19a9c81081&quot;]
  [&quot;0006-Coq-MenhirLib-explicit-import-ListNotations-354.patch&quot; &quot;sha256=3b7f59d4736d36878bbe3c0fed80e7db1ae75b9c8a5a9c90a57df2c1a4f4ae78&quot;]
  [&quot;0007-Use-ocamlfind-to-find-menhirLib.patch&quot; &quot;sha256=df3f103977fa02bd339f6a8537da6bd4eaf1baa54c9675508e3bd16dbe11464e&quot;]
  [&quot;0008-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch&quot; &quot;sha256=bcd2eb6eafb5a71fd0ee8ecf6f1b100b06723c636adb0ef2f915fa0ac3585c64&quot;]
  [&quot;0009-Don-t-build-MenhirLib-platform-version-is-used.patch&quot; &quot;sha256=77835a85124eb1e8afefdcaf9eaa5beab64ed0fea22fceab78b7fd550778c857&quot;]
]
install: [
  [make &quot;install&quot;]
]
depends: [
  &quot;coq&quot; {&gt;= &quot;8.12&quot; &amp; &lt; &quot;8.13&quot;}
  &quot;coq-flocq&quot; {&gt;= &quot;3.2.1&quot;}
  &quot;coq-menhirlib&quot; {&gt;= &quot;20190626&quot;}
  &quot;menhir&quot; {&gt;= &quot;20190626&quot;}
  &quot;ocaml&quot; {&gt;= &quot;4.05.0&quot;}
]
synopsis: &quot;The CompCert C compiler (using coq-platform supplied version of Flocq)&quot;
tags: [
  &quot;category:Computer Science/Semantics and Compilation/Compilation&quot;
  &quot;category:Computer Science/Semantics and Compilation/Semantics&quot;
  &quot;keyword:C&quot;
  &quot;keyword:compiler&quot;
  &quot;logpath:compcert&quot;
  &quot;date:2020-04-29&quot;
]
url {
  src: &quot;https://github.com/AbsInt/CompCert/archive/v3.7.tar.gz&quot;
  checksum: &quot;sha256=ceee1b2ed6c2576cb66eb7a0f2669dcf85e65c0fc68385f0781b0ca4edb87eb0&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-compcert.3.7+8.12~coq_platform coq.dev</code></dd>
              <dt>Return code</dt>
              <dd>5120</dd>
              <dt>Output</dt>
              <dd><pre>[NOTE] Package coq is already installed (current version is dev).
The following dependencies couldn&#39;t be met:
  - coq-compcert -&gt; coq &lt; 8.13 -&gt; ocaml &lt; 4.10
      base of this switch (use `--unlock-base&#39; to force)
Your request can&#39;t be satisfied:
  - No available version of coq satisfies the constraints
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-compcert.3.7+8.12~coq_platform</code></dd>
              <dt>Return code</dt>
              <dd>0</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">
          <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>
