-
Notifications
You must be signed in to change notification settings - Fork 167
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 #2893 from liyishuai/certicoq
Add coq-certicoq.dev
- Loading branch information
Showing
10 changed files
with
427 additions
and
0 deletions.
There are no files selected for viewing
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,45 @@ | ||
| opam-version: "2.0" | ||
| maintainer: "The CertiCoq Team" | ||
| homepage: "https://certicoq.org/" | ||
| dev-repo: "git+https://github.com/CertiCoq/certicoq" | ||
| bug-reports: "https://github.com/CertiCoq/certicoq/issues" | ||
| authors: ["Andrew Appel" | ||
| "Yannick Forster" | ||
| "Anvay Grover" | ||
| "Joomy Korkut" | ||
| "John Li" | ||
| "Zoe Paraskevopoulou" | ||
| "Matthieu Sozeau" | ||
| "Matthew Weaver" | ||
| "Abhishek Anand" | ||
| "Greg Morrisett" | ||
| "Randy Pollack" | ||
| "Olivier Savary Belanger" | ||
| ] | ||
| license: "MIT" | ||
| build: [ | ||
| ["bash" "./configure.sh"] | ||
| [make "all"] | ||
| [make "plugins"] | ||
| [make "bootstrap"] | ||
| [make "-C" "benchmarks" "all"] {with-test} | ||
| [make "-C" "bootstrap" "tests"] {with-test} | ||
| ] | ||
| install: [ | ||
| [make "install"] | ||
| ] | ||
| depends: [ | ||
| "ocaml" | ||
| "stdlib-shims" | ||
| "coq" {>= "8.17" & < "8.18~"} | ||
| "coq-compcert" {= "3.12"} | ||
| "coq-equations" {= "1.3+8.17"} | ||
| "coq-metacoq-erasure-plugin" {= "8.17.dev"} | ||
| "coq-metacoq-safechecker-plugin" {= "8.17.dev"} | ||
| "coq-ext-lib" {>= "0.11.8"} | ||
| ] | ||
|
|
||
| synopsis: "A Verified Compiler for Gallina, Written in Gallina " | ||
| url { | ||
| src: "git+https://github.com/CertiCoq/certicoq.git#master" | ||
| } |
38 changes: 38 additions & 0 deletions
38
extra-dev/packages/coq-metacoq-common/coq-metacoq-common.8.17.dev/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,38 @@ | ||
| opam-version: "2.0" | ||
| maintainer: "[email protected]" | ||
| homepage: "https://metacoq.github.io/metacoq" | ||
| dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.17" | ||
| 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]>" | ||
| "Jason Gross <[email protected]>" | ||
| "Fabian Kunze <[email protected]>" | ||
| "Meven Lennon-Bertrand <[email protected]>" | ||
| "Kenji Maillard <[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}%" "-C" "common"] | ||
| ] | ||
| install: [ | ||
| [make "-C" "common" "install"] | ||
| ] | ||
| depends: [ | ||
| "coq-metacoq-utils" {= version} | ||
| ] | ||
| synopsis: "The common library of Template Coq and PCUIC" | ||
| description: """ | ||
| MetaCoq is a meta-programming framework for Coq. | ||
| """ | ||
| url { | ||
| src: "git+https:///github.com/metacoq/metacoq.git#coq-8.17" | ||
| } |
47 changes: 47 additions & 0 deletions
47
extra-dev/packages/coq-metacoq-erasure-plugin/coq-metacoq-erasure-plugin.8.17.dev/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.17" | ||
| 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]>" | ||
| "Jason Gross <[email protected]>" | ||
| "Fabian Kunze <[email protected]>" | ||
| "Meven Lennon-Bertrand <[email protected]>" | ||
| "Kenji Maillard <[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}%" "-C" "erasure-plugin"] | ||
| ] | ||
| install: [ | ||
| [make "-C" "erasure-plugin" "install"] | ||
| ] | ||
| depends: [ | ||
| "coq-metacoq-template-pcuic" {= version} | ||
| "coq-metacoq-erasure" {= 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: "git+https:///github.com/metacoq/metacoq.git#coq-8.17" | ||
| } |
47 changes: 47 additions & 0 deletions
47
extra-dev/packages/coq-metacoq-erasure/coq-metacoq-erasure.8.17.dev/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.17" | ||
| 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]>" | ||
| "Jason Gross <[email protected]>" | ||
| "Fabian Kunze <[email protected]>" | ||
| "Meven Lennon-Bertrand <[email protected]>" | ||
| "Kenji Maillard <[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}%" "-C" "erasure"] | ||
| ] | ||
| install: [ | ||
| [make "-C" "erasure" "install"] | ||
| ] | ||
| depends: [ | ||
| "coq-metacoq-safechecker" {= version} | ||
| "coq-metacoq-template-pcuic" {= 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: "git+https:///github.com/metacoq/metacoq.git#coq-8.17" | ||
| } |
42 changes: 42 additions & 0 deletions
42
extra-dev/packages/coq-metacoq-pcuic/coq-metacoq-pcuic.8.17.dev/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,42 @@ | ||
| opam-version: "2.0" | ||
| maintainer: "[email protected]" | ||
| homepage: "https://metacoq.github.io/metacoq" | ||
| dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.17" | ||
| 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]>" | ||
| "Jason Gross <[email protected]>" | ||
| "Fabian Kunze <[email protected]>" | ||
| "Meven Lennon-Bertrand <[email protected]>" | ||
| "Kenji Maillard <[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}%" "-C" "pcuic"] | ||
| ] | ||
| install: [ | ||
| [make "-C" "pcuic" "install"] | ||
| ] | ||
| depends: [ | ||
| "coq-metacoq-common" {= 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: "git+https:///github.com/metacoq/metacoq.git#coq-8.17" | ||
| } |
47 changes: 47 additions & 0 deletions
47
...-dev/packages/coq-metacoq-safechecker-plugin/coq-metacoq-safechecker-plugin.8.17.dev/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.17" | ||
| 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]>" | ||
| "Jason Gross <[email protected]>" | ||
| "Fabian Kunze <[email protected]>" | ||
| "Meven Lennon-Bertrand <[email protected]>" | ||
| "Kenji Maillard <[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}%" "-C" "safechecker-plugin"] | ||
| ] | ||
| install: [ | ||
| [make "-C" "safechecker-plugin" "install"] | ||
| ] | ||
| depends: [ | ||
| "coq-metacoq-template-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: "git+https:///github.com/metacoq/metacoq.git#coq-8.17" | ||
| } |
41 changes: 41 additions & 0 deletions
41
extra-dev/packages/coq-metacoq-safechecker/coq-metacoq-safechecker.8.17.dev/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.17" | ||
| 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]>" | ||
| "Jason Gross <[email protected]>" | ||
| "Fabian Kunze <[email protected]>" | ||
| "Meven Lennon-Bertrand <[email protected]>" | ||
| "Kenji Maillard <[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}%" "-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: "git+https:///github.com/metacoq/metacoq.git#coq-8.17" | ||
| } |
38 changes: 38 additions & 0 deletions
38
extra-dev/packages/coq-metacoq-template-pcuic/coq-metacoq-template-pcuic.8.17.dev/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,38 @@ | ||
| opam-version: "2.0" | ||
| maintainer: "[email protected]" | ||
| homepage: "https://metacoq.github.io/metacoq" | ||
| dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.17" | ||
| 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]>" | ||
| "Jason Gross <[email protected]>" | ||
| "Fabian Kunze <[email protected]>" | ||
| "Meven Lennon-Bertrand <[email protected]>" | ||
| "Kenji Maillard <[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}%" "-C" "template-pcuic"] | ||
| ] | ||
| install: [ | ||
| [make "-C" "template-pcuic" "install"] | ||
| ] | ||
| depends: [ | ||
| "coq-metacoq-template" {= version} | ||
| "coq-metacoq-pcuic" {= version} | ||
| ] | ||
| synopsis: "Translations between Template Coq and PCUIC and proofs of correctness" | ||
| description: """ | ||
| """ | ||
| url { | ||
| src: "git+https:///github.com/metacoq/metacoq.git#coq-8.17" | ||
| } |
42 changes: 42 additions & 0 deletions
42
extra-dev/packages/coq-metacoq-template/coq-metacoq-template.8.17.dev/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,42 @@ | ||
| opam-version: "2.0" | ||
| maintainer: "[email protected]" | ||
| homepage: "https://metacoq.github.io/metacoq" | ||
| dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.17" | ||
| 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]>" | ||
| "Jason Gross <[email protected]>" | ||
| "Fabian Kunze <[email protected]>" | ||
| "Meven Lennon-Bertrand <[email protected]>" | ||
| "Kenji Maillard <[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}%" "-C" "pcuic"] | ||
| ] | ||
| install: [ | ||
| [make "-C" "pcuic" "install"] | ||
| ] | ||
| depends: [ | ||
| "coq-metacoq-common" {= 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: "git+https:///github.com/metacoq/metacoq.git#coq-8.17" | ||
| } |
Oops, something went wrong.