-
Notifications
You must be signed in to change notification settings - Fork 166
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #2216 from mattam82/metacoq-1.0+8.16
MetaCoq 1.0 for Coq 8.16
- Loading branch information
Showing
6 changed files
with
261 additions
and
0 deletions.
There are no files selected for viewing
47 changes: 47 additions & 0 deletions
47
extra-dev/packages/coq-metacoq-erasure/coq-metacoq-erasure.1.0+8.16/opam
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,47 @@ | ||
| opam-version: "2.0" | ||
| maintainer: "[email protected]" | ||
| homepage: "https://metacoq.github.io/metacoq" | ||
| dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.16" | ||
| bug-reports: "https://github.com/MetaCoq/metacoq/issues" | ||
| authors: ["Abhishek Anand <[email protected]>" | ||
| "Danil Annenkov <[email protected]>" | ||
| "Simon Boulier <[email protected]>" | ||
| "Cyril Cohen <[email protected]>" | ||
| "Yannick Forster <[email protected]>" | ||
| "Fabian Kunze <[email protected]>" | ||
| "Meven Lennon-Bertrand <[email protected]>" | ||
| "Gregory Malecha <[email protected]>" | ||
| "Jakob Botsch Nielsen <[email protected]>" | ||
| "Matthieu Sozeau <[email protected]>" | ||
| "Nicolas Tabareau <[email protected]>" | ||
| "Théo Winterhalter <[email protected]>" | ||
| ] | ||
| license: "MIT" | ||
| build: [ | ||
| ["sh" "./configure.sh"] | ||
| [make "-j" "%{jobs}%" "-C" "erasure"] | ||
| ] | ||
| install: [ | ||
| [make "-C" "erasure" "install"] | ||
| ] | ||
| depends: [ | ||
| "coq-metacoq-template" {= version} | ||
| "coq-metacoq-pcuic" {= version} | ||
| "coq-metacoq-safechecker" {= version} | ||
| ] | ||
| synopsis: "Implementation and verification of an erasure procedure for Coq" | ||
| description: """ | ||
| MetaCoq is a meta-programming framework for Coq. | ||
|
|
||
| The Erasure module provides a complete specification of Coq's so-called | ||
| \"extraction\" procedure, starting from the PCUIC calculus and targeting | ||
| untyped call-by-value lambda-calculus. | ||
|
|
||
| The `erasure` function translates types and proofs in well-typed terms | ||
| into a dummy `tBox` constructor, following closely P. Letouzey's PhD | ||
| thesis. | ||
| """ | ||
| url { | ||
| src: "https://github.com/MetaCoq/metacoq/archive/refs/tags/v1.0-8.16.tar.gz" | ||
| checksum: "sha512=84c59b74d7ed3798593026d00e412ce2a9d1443afdaf98f5f680788ed8e73cf7e67dcd91392efe2243c5cd61b979edea9bf109f72ea5c45de5c31ef732bba593" | ||
| } |
41 changes: 41 additions & 0 deletions
41
extra-dev/packages/coq-metacoq-pcuic/coq-metacoq-pcuic.1.0+8.16/opam
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,41 @@ | ||
| opam-version: "2.0" | ||
| maintainer: "[email protected]" | ||
| homepage: "https://metacoq.github.io/metacoq" | ||
| dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.16" | ||
| bug-reports: "https://github.com/MetaCoq/metacoq/issues" | ||
| authors: ["Abhishek Anand <[email protected]>" | ||
| "Danil Annenkov <[email protected]>" | ||
| "Simon Boulier <[email protected]>" | ||
| "Cyril Cohen <[email protected]>" | ||
| "Yannick Forster <[email protected]>" | ||
| "Fabian Kunze <[email protected]>" | ||
| "Meven Lennon-Bertrand <[email protected]>" | ||
| "Gregory Malecha <[email protected]>" | ||
| "Jakob Botsch Nielsen <[email protected]>" | ||
| "Matthieu Sozeau <[email protected]>" | ||
| "Nicolas Tabareau <[email protected]>" | ||
| "Théo Winterhalter <[email protected]>" | ||
| ] | ||
| license: "MIT" | ||
| build: [ | ||
| ["sh" "./configure.sh"] | ||
| [make "-j" "%{jobs}%" "-C" "pcuic"] | ||
| ] | ||
| install: [ | ||
| [make "-C" "pcuic" "install"] | ||
| ] | ||
| depends: [ | ||
| "coq-metacoq-template" {= version} | ||
| ] | ||
| synopsis: "A type system equivalent to Coq's and its metatheory" | ||
| description: """ | ||
| MetaCoq is a meta-programming framework for Coq. | ||
|
|
||
| The PCUIC module provides a cleaned-up specification of Coq's typing algorithm along | ||
| with a certified typechecker for it. This module includes the standard metatheory of | ||
| PCUIC: Weakening, Substitution, Confluence and Subject Reduction are proven here. | ||
| """ | ||
| url { | ||
| src: "https://github.com/MetaCoq/metacoq/archive/refs/tags/v1.0-8.16.tar.gz" | ||
| checksum: "sha512=84c59b74d7ed3798593026d00e412ce2a9d1443afdaf98f5f680788ed8e73cf7e67dcd91392efe2243c5cd61b979edea9bf109f72ea5c45de5c31ef732bba593" | ||
| } |
40 changes: 40 additions & 0 deletions
40
extra-dev/packages/coq-metacoq-safechecker/coq-metacoq-safechecker.1.0+8.16/opam
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,40 @@ | ||
| opam-version: "2.0" | ||
| maintainer: "[email protected]" | ||
| homepage: "https://metacoq.github.io/metacoq" | ||
| dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.16" | ||
| bug-reports: "https://github.com/MetaCoq/metacoq/issues" | ||
| authors: ["Abhishek Anand <[email protected]>" | ||
| "Danil Annenkov <[email protected]>" | ||
| "Simon Boulier <[email protected]>" | ||
| "Cyril Cohen <[email protected]>" | ||
| "Yannick Forster <[email protected]>" | ||
| "Fabian Kunze <[email protected]>" | ||
| "Meven Lennon-Bertrand <[email protected]>" | ||
| "Gregory Malecha <[email protected]>" | ||
| "Jakob Botsch Nielsen <[email protected]>" | ||
| "Matthieu Sozeau <[email protected]>" | ||
| "Nicolas Tabareau <[email protected]>" | ||
| "Théo Winterhalter <[email protected]>" | ||
| ] | ||
| license: "MIT" | ||
| build: [ | ||
| ["sh" "./configure.sh"] | ||
| [make "-j" "%{jobs}%" "-C" "safechecker"] | ||
| ] | ||
| install: [ | ||
| [make "-C" "safechecker" "install"] | ||
| ] | ||
| depends: [ | ||
| "coq-metacoq-pcuic" {= version} | ||
| ] | ||
| synopsis: "Implementation and verification of safe conversion and typechecking algorithms for Coq" | ||
| description: """ | ||
| MetaCoq is a meta-programming framework for Coq. | ||
|
|
||
| The SafeChecker modules provides a correct implementation of | ||
| weak-head reduction, conversion and typechecking of Coq definitions and global environments. | ||
| """ | ||
| url { | ||
| src: "https://github.com/MetaCoq/metacoq/archive/refs/tags/v1.0-8.16.tar.gz" | ||
| checksum: "sha512=84c59b74d7ed3798593026d00e412ce2a9d1443afdaf98f5f680788ed8e73cf7e67dcd91392efe2243c5cd61b979edea9bf109f72ea5c45de5c31ef732bba593" | ||
| } |
52 changes: 52 additions & 0 deletions
52
extra-dev/packages/coq-metacoq-template/coq-metacoq-template.1.0+8.16/opam
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,52 @@ | ||
| opam-version: "2.0" | ||
| maintainer: "[email protected]" | ||
| homepage: "https://metacoq.github.io/metacoq" | ||
| dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.16" | ||
| bug-reports: "https://github.com/MetaCoq/metacoq/issues" | ||
| authors: ["Abhishek Anand <[email protected]>" | ||
| "Danil Annenkov <[email protected]>" | ||
| "Simon Boulier <[email protected]>" | ||
| "Cyril Cohen <[email protected]>" | ||
| "Yannick Forster <[email protected]>" | ||
| "Fabian Kunze <[email protected]>" | ||
| "Meven Lennon-Bertrand <[email protected]>" | ||
| "Gregory Malecha <[email protected]>" | ||
| "Jakob Botsch Nielsen <[email protected]>" | ||
| "Matthieu Sozeau <[email protected]>" | ||
| "Nicolas Tabareau <[email protected]>" | ||
| "Théo Winterhalter <[email protected]>" | ||
| ] | ||
| license: "MIT" | ||
| build: [ | ||
| ["bash" "./configure.sh"] | ||
| [make "-j" "%{jobs}%" "template-coq"] | ||
| ] | ||
| install: [ | ||
| [make "-C" "template-coq" "install"] | ||
| ] | ||
| depends: [ | ||
| "stdlib-shims" | ||
| "coq" { >= "8.16" & < "8.17~" } | ||
| "coq-equations" { >= "1.3" } | ||
| ] | ||
| synopsis: "A quoting and unquoting library for Coq in Coq" | ||
| description: """ | ||
| MetaCoq is a meta-programming framework for Coq. | ||
|
|
||
| Template Coq is a quoting library for Coq. It takes Coq terms and | ||
| constructs a representation of their syntax tree as a Coq inductive data | ||
| type. The representation is based on the kernel's term representation. | ||
|
|
||
| In addition to a complete reification and denotation of CIC terms, | ||
| Template Coq includes: | ||
|
|
||
| - Reification of the environment structures, for constant and inductive declarations. | ||
| - Denotation of terms and global declarations | ||
| - A monad for manipulating global declarations, calling the type | ||
| checker, and inserting them in the global environment, in the style of | ||
| MetaCoq/MTac. | ||
| """ | ||
| url { | ||
| src: "https://github.com/MetaCoq/metacoq/archive/refs/tags/v1.0-8.16.tar.gz" | ||
| checksum: "sha512=84c59b74d7ed3798593026d00e412ce2a9d1443afdaf98f5f680788ed8e73cf7e67dcd91392efe2243c5cd61b979edea9bf109f72ea5c45de5c31ef732bba593" | ||
| } |
41 changes: 41 additions & 0 deletions
41
extra-dev/packages/coq-metacoq-translations/coq-metacoq-translations.1.0+8.16/opam
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,41 @@ | ||
| opam-version: "2.0" | ||
| maintainer: "[email protected]" | ||
| homepage: "https://metacoq.github.io/metacoq" | ||
| dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.16" | ||
| bug-reports: "https://github.com/MetaCoq/metacoq/issues" | ||
| authors: ["Abhishek Anand <[email protected]>" | ||
| "Danil Annenkov <[email protected]>" | ||
| "Simon Boulier <[email protected]>" | ||
| "Cyril Cohen <[email protected]>" | ||
| "Yannick Forster <[email protected]>" | ||
| "Fabian Kunze <[email protected]>" | ||
| "Meven Lennon-Bertrand <[email protected]>" | ||
| "Gregory Malecha <[email protected]>" | ||
| "Jakob Botsch Nielsen <[email protected]>" | ||
| "Matthieu Sozeau <[email protected]>" | ||
| "Nicolas Tabareau <[email protected]>" | ||
| "Théo Winterhalter <[email protected]>" | ||
| ] | ||
| license: "MIT" | ||
| build: [ | ||
| ["sh" "./configure.sh"] | ||
| [make "-j" "%{jobs}%" "-C" "translations"] | ||
| ] | ||
| install: [ | ||
| [make "-C" "translations" "install"] | ||
| ] | ||
| depends: [ | ||
| "coq-metacoq-template" {= version} | ||
| ] | ||
| synopsis: "Translations built on top of MetaCoq" | ||
| description: """ | ||
| MetaCoq is a meta-programming framework for Coq. | ||
|
|
||
| The Translations modules provides implementation of standard translations | ||
| from type theory to type theory, e.g. parametricity and the `cross-bool` | ||
| translation that invalidates functional extensionality. | ||
| """ | ||
| url { | ||
| src: "https://github.com/MetaCoq/metacoq/archive/refs/tags/v1.0-8.16.tar.gz" | ||
| checksum: "sha512=84c59b74d7ed3798593026d00e412ce2a9d1443afdaf98f5f680788ed8e73cf7e67dcd91392efe2243c5cd61b979edea9bf109f72ea5c45de5c31ef732bba593" | ||
| } |
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,40 @@ | ||
| opam-version: "2.0" | ||
| maintainer: "[email protected]" | ||
| homepage: "https://metacoq.github.io/metacoq" | ||
| dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.16" | ||
| bug-reports: "https://github.com/MetaCoq/metacoq/issues" | ||
| authors: ["Abhishek Anand <[email protected]>" | ||
| "Danil Annenkov <[email protected]>" | ||
| "Simon Boulier <[email protected]>" | ||
| "Cyril Cohen <[email protected]>" | ||
| "Yannick Forster <[email protected]>" | ||
| "Fabian Kunze <[email protected]>" | ||
| "Meven Lennon-Bertrand <[email protected]>" | ||
| "Gregory Malecha <[email protected]>" | ||
| "Jakob Botsch Nielsen <[email protected]>" | ||
| "Matthieu Sozeau <[email protected]>" | ||
| "Nicolas Tabareau <[email protected]>" | ||
| "Théo Winterhalter <[email protected]>" | ||
| ] | ||
| license: "MIT" | ||
| depends: [ | ||
| "coq-metacoq-template" {= version} | ||
| "coq-metacoq-pcuic" {= version} | ||
| "coq-metacoq-safechecker" {= version} | ||
| "coq-metacoq-erasure" {= version} | ||
| "coq-metacoq-translations" {= version} | ||
| ] | ||
| synopsis: "A meta-programming framework for Coq" | ||
| description: """ | ||
| MetaCoq is a meta-programming framework for Coq. | ||
|
|
||
| The meta-package includes the template-coq library, | ||
| the PCUIC development including a verified equivalence between Coq and PCUIC, | ||
| a safe type checker and verified erasure for PCUIC and example translations. | ||
|
|
||
| See individual packages for more detailed descriptions. | ||
| """ | ||
| url { | ||
| src: "https://github.com/MetaCoq/metacoq/archive/refs/tags/v1.0-8.16.tar.gz" | ||
| checksum: "sha512=84c59b74d7ed3798593026d00e412ce2a9d1443afdaf98f5f680788ed8e73cf7e67dcd91392efe2243c5cd61b979edea9bf109f72ea5c45de5c31ef732bba593" | ||
| } |