-
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.17.0, repo released, mode clean.
- Loading branch information
Bench B. Bench
committed
Feb 1, 2024
1 parent
e674d7b
commit 65be3ca
Showing
5,359 changed files
with
600,416 additions
and
36,718 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
181 changes: 181 additions & 0 deletions
181
clean/Linux-x86_64-4.13.1-2.0.10/released/8.16.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,181 @@ | ||
| <!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.16.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-threads base | ||
| base-unix base | ||
| conf-findutils 1 Virtual package relying on findutils | ||
| conf-gmp 4 Virtual package relying on a GMP lib system installation | ||
| coq 8.16.0 Formal proof management system | ||
| dune 3.13.0 Fast, portable, and opinionated build system | ||
| ocaml 4.13.1 The OCaml compiler (virtual package) | ||
| ocaml-base-compiler 4.13.1 Official release 4.13.1 | ||
| ocaml-config 2 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.16.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.16.0). | ||
| The following dependencies couldn't be met: | ||
| - coq-aac-tactics -> coq < 8.11~ -> ocaml < 4.10 | ||
| base of this switch (use `--unlock-base' 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-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> |
180 changes: 180 additions & 0 deletions
180
clean/Linux-x86_64-4.13.1-2.0.10/released/8.16.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,180 @@ | ||
| <!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.16.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-threads base | ||
| base-unix base | ||
| conf-findutils 1 Virtual package relying on findutils | ||
| conf-gmp 4 Virtual package relying on a GMP lib system installation | ||
| coq 8.16.0 Formal proof management system | ||
| dune 3.13.0 Fast, portable, and opinionated build system | ||
| ocaml 4.13.1 The OCaml compiler (virtual package) | ||
| ocaml-base-compiler 4.13.1 Official release 4.13.1 | ||
| ocaml-config 2 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.16.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.16.0). | ||
| The following dependencies couldn't be met: | ||
| - coq-aac-tactics -> coq < 8.12~ -> ocaml < 4.12 | ||
| base of this switch (use `--unlock-base' 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-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.