-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Coq 8.19.0, repo released, mode clean.
- Loading branch information
Bench B. Bench
committed
Feb 20, 2024
1 parent
157355b
commit c978fb1
Showing
5,429 changed files
with
554,508 additions
and
11,324 deletions.
The diff you're trying to view is too large. We only load the first 3000 changed files.
There are no files selected for viewing
194 changes: 194 additions & 0 deletions
194
clean/Linux-x86_64-5.0.0-2.1.5/released/8.19.0/aac-tactics/8.10.0.html
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,194 @@ | ||
| <!DOCTYPE html> | ||
| <html lang="en"> | ||
| <head> | ||
| <meta charset="utf-8"> | ||
| <meta name="viewport" content="width=device-width, initial-scale=1"> | ||
| <title>aac-tactics: 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 / released</a></li> | ||
| <li class="active"><a href="">8.19.0 / aac-tactics - 8.10.0</a></li> | ||
| </ul> | ||
| </div> | ||
| </div> | ||
| </div> | ||
| <div class="article"> | ||
| <div class="row"> | ||
| <div class="col-md-12"> | ||
| <a href="../..">« Up</a> | ||
| <h1> | ||
| aac-tactics | ||
| <small> | ||
| 8.10.0 | ||
| <span class="label label-info">Not compatible 👼</span> | ||
| </small> | ||
| </h1> | ||
| <h2>Context</h2> | ||
| <pre># Packages matching: installed | ||
| # Name # Installed # Synopsis | ||
| base-bigarray base | ||
| base-domains base | ||
| base-nnp base Naked pointers prohibited in the OCaml heap | ||
| base-threads base | ||
| base-unix base | ||
| conf-gmp 4 Virtual package relying on a GMP lib system installation | ||
| conf-linux-libc-dev 0 Virtual package relying on the installation of the Linux kernel headers files | ||
| coq 8.19.0 The Coq Proof Assistant | ||
| coq-core 8.19.0 The Coq Proof Assistant -- Core Binaries and Tools | ||
| coq-stdlib 8.19.0 The Coq Proof Assistant -- Standard Library | ||
| coqide-server 8.19.0 The Coq Proof Assistant, XML protocol server | ||
| dune 3.14.0 Fast, portable, and opinionated build system | ||
| ocaml 5.0.0 The OCaml compiler (virtual package) | ||
| ocaml-base-compiler 5.0.0 Official release 5.0.0 | ||
| ocaml-config 3 OCaml Switch Configuration | ||
| ocaml-options-vanilla 1 Ensure that OCaml is compiled with no special options enabled | ||
| ocamlfind 1.9.6 A library manager for OCaml | ||
| zarith 1.13 Implements arithmetic and logical operations over arbitrary-precision integers | ||
| # opam file: | ||
| opam-version: "2.0" | ||
| maintainer: "[email protected]" | ||
| homepage: "https://github.com/coq-community/aac-tactics" | ||
| dev-repo: "git+https://github.com/coq-community/aac-tactics.git" | ||
| bug-reports: "https://github.com/coq-community/aac-tactics/issues" | ||
| license: "LGPL-3.0-or-later" | ||
| synopsis: "This Coq plugin provides tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators" | ||
| description: """ | ||
| This Coq plugin provides tactics for rewriting universally quantified | ||
| equations, modulo associativity and commutativity of some operator. | ||
| The tactics can be applied for custom operators by registering the | ||
| operators and their properties as type class instances. Many common | ||
| operator instances, such as for Z binary arithmetic and booleans, are | ||
| provided with the plugin. | ||
| """ | ||
| build: [make "-j%{jobs}%"] | ||
| install: [make "install"] | ||
| depends: [ | ||
| "ocaml" | ||
| "coq" {>= "8.10" & < "8.11~"} | ||
| ] | ||
| tags: [ | ||
| "category:Miscellaneous/Coq Extensions" | ||
| "category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures" | ||
| "keyword:reflexive tactic" | ||
| "keyword:rewriting" | ||
| "keyword:rewriting modulo associativity and commutativity" | ||
| "keyword:rewriting modulo ac" | ||
| "keyword:decision procedure" | ||
| "logpath:AAC_tactics" | ||
| "date:2019-10-17" | ||
| ] | ||
| authors: [ | ||
| "Thomas Braibant" | ||
| "Damien Pous" | ||
| "Fabian Kunze" | ||
| ] | ||
| url { | ||
| src: "https://github.com/coq-community/aac-tactics/archive/v8.10.0.tar.gz" | ||
| checksum: "sha512=45db1f57d1ecb3aaddc59fe51d3251288429dbf3dbb432331325fd5ecc23eb7595f0c0abcef22ff172c1f12e5fe8407f5546a859cd5efc1db47dc7ee7effa6ee" | ||
| } | ||
| </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-aac-tactics.8.10.0 coq.8.19.0</code></dd> | ||
| <dt>Return code</dt> | ||
| <dd>5120</dd> | ||
| <dt>Output</dt> | ||
| <dd><pre>[NOTE] Package coq is already installed (current version is 8.19.0). | ||
| [ERROR] Package conflict! | ||
| * No agreement on the version of ocaml: | ||
| - (invariant) -> ocaml-base-compiler = 5.0.0 -> ocaml = 5.0.0 | ||
| - coq-aac-tactics = 8.10.0 -> coq < 8.11~ -> ocaml < 4.02.0 | ||
| You can temporarily relax the switch invariant with `--update-invariant' | ||
| * No agreement on the version of ocaml-base-compiler: | ||
| - (invariant) -> ocaml-base-compiler = 5.0.0 | ||
| - coq-aac-tactics = 8.10.0 -> coq < 8.11~ -> ocaml < 4.02.0 -> ocaml-base-compiler = 3.07+1 | ||
| * Missing dependency: | ||
| - coq-aac-tactics = 8.10.0 -> coq < 8.11~ -> ocaml < 4.02.0 -> ocaml-variants >= 3.09.2 -> ocaml-beta | ||
| unmet availability conditions: 'enable-ocaml-beta-repository' | ||
| 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-aac-tactics.8.10.0</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"> | ||
| 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> |
193 changes: 193 additions & 0 deletions
193
clean/Linux-x86_64-5.0.0-2.1.5/released/8.19.0/aac-tactics/8.11.0.html
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,193 @@ | ||
| <!DOCTYPE html> | ||
| <html lang="en"> | ||
| <head> | ||
| <meta charset="utf-8"> | ||
| <meta name="viewport" content="width=device-width, initial-scale=1"> | ||
| <title>aac-tactics: 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 / released</a></li> | ||
| <li class="active"><a href="">8.19.0 / aac-tactics - 8.11.0</a></li> | ||
| </ul> | ||
| </div> | ||
| </div> | ||
| </div> | ||
| <div class="article"> | ||
| <div class="row"> | ||
| <div class="col-md-12"> | ||
| <a href="../..">« Up</a> | ||
| <h1> | ||
| aac-tactics | ||
| <small> | ||
| 8.11.0 | ||
| <span class="label label-info">Not compatible 👼</span> | ||
| </small> | ||
| </h1> | ||
| <h2>Context</h2> | ||
| <pre># Packages matching: installed | ||
| # Name # Installed # Synopsis | ||
| base-bigarray base | ||
| base-domains base | ||
| base-nnp base Naked pointers prohibited in the OCaml heap | ||
| base-threads base | ||
| base-unix base | ||
| conf-gmp 4 Virtual package relying on a GMP lib system installation | ||
| conf-linux-libc-dev 0 Virtual package relying on the installation of the Linux kernel headers files | ||
| coq 8.19.0 The Coq Proof Assistant | ||
| coq-core 8.19.0 The Coq Proof Assistant -- Core Binaries and Tools | ||
| coq-stdlib 8.19.0 The Coq Proof Assistant -- Standard Library | ||
| coqide-server 8.19.0 The Coq Proof Assistant, XML protocol server | ||
| dune 3.14.0 Fast, portable, and opinionated build system | ||
| ocaml 5.0.0 The OCaml compiler (virtual package) | ||
| ocaml-base-compiler 5.0.0 Official release 5.0.0 | ||
| ocaml-config 3 OCaml Switch Configuration | ||
| ocaml-options-vanilla 1 Ensure that OCaml is compiled with no special options enabled | ||
| ocamlfind 1.9.6 A library manager for OCaml | ||
| zarith 1.13 Implements arithmetic and logical operations over arbitrary-precision integers | ||
| # opam file: | ||
| opam-version: "2.0" | ||
| maintainer: "[email protected]" | ||
| homepage: "https://github.com/coq-community/aac-tactics" | ||
| dev-repo: "git+https://github.com/coq-community/aac-tactics.git" | ||
| bug-reports: "https://github.com/coq-community/aac-tactics/issues" | ||
| license: "LGPL-3.0-or-later" | ||
| synopsis: "This Coq plugin provides tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators" | ||
| description: """ | ||
| This Coq plugin provides tactics for rewriting universally quantified | ||
| equations, modulo associativity and commutativity of some operator. | ||
| The tactics can be applied for custom operators by registering the | ||
| operators and their properties as type class instances. Many common | ||
| operator instances, such as for Z binary arithmetic and booleans, are | ||
| provided with the plugin.""" | ||
| build: [make "-j%{jobs}%"] | ||
| install: [make "install"] | ||
| depends: [ | ||
| "ocaml" {>= "4.05.0"} | ||
| "coq" {>= "8.11" & < "8.12~"} | ||
| ] | ||
| tags: [ | ||
| "category:Miscellaneous/Coq Extensions" | ||
| "category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures" | ||
| "keyword:reflexive tactic" | ||
| "keyword:rewriting" | ||
| "keyword:rewriting modulo associativity and commutativity" | ||
| "keyword:rewriting modulo ac" | ||
| "keyword:decision procedure" | ||
| "logpath:AAC_tactics" | ||
| "date:2020-01-31" | ||
| ] | ||
| authors: [ | ||
| "Thomas Braibant" | ||
| "Damien Pous" | ||
| "Fabian Kunze" | ||
| ] | ||
| url { | ||
| src: "https://github.com/coq-community/aac-tactics/archive/v8.11.0.tar.gz" | ||
| checksum: "sha512=91d8d83bef9d1156ec42b3ed02b6457cd776c4b1a6d93f2b64cb234ef96c044fa85052a6adc68acb0670a93574b80291d4abac80bd8eb694e2cb23e9fa880e92" | ||
| } | ||
| </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-aac-tactics.8.11.0 coq.8.19.0</code></dd> | ||
| <dt>Return code</dt> | ||
| <dd>5120</dd> | ||
| <dt>Output</dt> | ||
| <dd><pre>[NOTE] Package coq is already installed (current version is 8.19.0). | ||
| [ERROR] Package conflict! | ||
| * No agreement on the version of ocaml: | ||
| - (invariant) -> ocaml-base-compiler = 5.0.0 -> ocaml = 5.0.0 | ||
| - coq-aac-tactics = 8.11.0 -> coq < 8.12~ -> ocaml < 4.02.0 | ||
| You can temporarily relax the switch invariant with `--update-invariant' | ||
| * No agreement on the version of ocaml-base-compiler: | ||
| - (invariant) -> ocaml-base-compiler = 5.0.0 | ||
| - coq-aac-tactics = 8.11.0 -> coq < 8.12~ -> ocaml < 4.02.0 -> ocaml-base-compiler = 3.07+1 | ||
| * Missing dependency: | ||
| - coq-aac-tactics = 8.11.0 -> coq < 8.12~ -> ocaml < 4.02.0 -> ocaml-variants >= 3.09.2 -> ocaml-beta | ||
| unmet availability conditions: 'enable-ocaml-beta-repository' | ||
| 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-aac-tactics.8.11.0</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"> | ||
| 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> |
Oops, something went wrong.