diff --git a/extra-dev/packages/coq-certicoq/coq-certicoq.dev/opam b/extra-dev/packages/coq-certicoq/coq-certicoq.dev/opam new file mode 100644 index 000000000..952f3df2b --- /dev/null +++ b/extra-dev/packages/coq-certicoq/coq-certicoq.dev/opam @@ -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" +} diff --git a/extra-dev/packages/coq-metacoq-common/coq-metacoq-common.8.17.dev/opam b/extra-dev/packages/coq-metacoq-common/coq-metacoq-common.8.17.dev/opam new file mode 100644 index 000000000..2d202bf98 --- /dev/null +++ b/extra-dev/packages/coq-metacoq-common/coq-metacoq-common.8.17.dev/opam @@ -0,0 +1,38 @@ +opam-version: "2.0" +maintainer: "matthieu.sozeau@inria.fr" +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 " + "Danil Annenkov " + "Simon Boulier " + "Cyril Cohen " + "Yannick Forster " + "Jason Gross " + "Fabian Kunze " + "Meven Lennon-Bertrand " + "Kenji Maillard " + "Gregory Malecha " + "Jakob Botsch Nielsen " + "Matthieu Sozeau " + "Nicolas Tabareau " + "Théo Winterhalter " +] +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" +} diff --git a/extra-dev/packages/coq-metacoq-erasure-plugin/coq-metacoq-erasure-plugin.8.17.dev/opam b/extra-dev/packages/coq-metacoq-erasure-plugin/coq-metacoq-erasure-plugin.8.17.dev/opam new file mode 100644 index 000000000..e671b2d87 --- /dev/null +++ b/extra-dev/packages/coq-metacoq-erasure-plugin/coq-metacoq-erasure-plugin.8.17.dev/opam @@ -0,0 +1,47 @@ +opam-version: "2.0" +maintainer: "matthieu.sozeau@inria.fr" +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 " + "Danil Annenkov " + "Simon Boulier " + "Cyril Cohen " + "Yannick Forster " + "Jason Gross " + "Fabian Kunze " + "Meven Lennon-Bertrand " + "Kenji Maillard " + "Gregory Malecha " + "Jakob Botsch Nielsen " + "Matthieu Sozeau " + "Nicolas Tabareau " + "Théo Winterhalter " +] +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" +} diff --git a/extra-dev/packages/coq-metacoq-erasure/coq-metacoq-erasure.8.17.dev/opam b/extra-dev/packages/coq-metacoq-erasure/coq-metacoq-erasure.8.17.dev/opam new file mode 100644 index 000000000..e0b16d093 --- /dev/null +++ b/extra-dev/packages/coq-metacoq-erasure/coq-metacoq-erasure.8.17.dev/opam @@ -0,0 +1,47 @@ +opam-version: "2.0" +maintainer: "matthieu.sozeau@inria.fr" +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 " + "Danil Annenkov " + "Simon Boulier " + "Cyril Cohen " + "Yannick Forster " + "Jason Gross " + "Fabian Kunze " + "Meven Lennon-Bertrand " + "Kenji Maillard " + "Gregory Malecha " + "Jakob Botsch Nielsen " + "Matthieu Sozeau " + "Nicolas Tabareau " + "Théo Winterhalter " +] +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" +} diff --git a/extra-dev/packages/coq-metacoq-pcuic/coq-metacoq-pcuic.8.17.dev/opam b/extra-dev/packages/coq-metacoq-pcuic/coq-metacoq-pcuic.8.17.dev/opam new file mode 100644 index 000000000..9181754b5 --- /dev/null +++ b/extra-dev/packages/coq-metacoq-pcuic/coq-metacoq-pcuic.8.17.dev/opam @@ -0,0 +1,42 @@ +opam-version: "2.0" +maintainer: "matthieu.sozeau@inria.fr" +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 " + "Danil Annenkov " + "Simon Boulier " + "Cyril Cohen " + "Yannick Forster " + "Jason Gross " + "Fabian Kunze " + "Meven Lennon-Bertrand " + "Kenji Maillard " + "Gregory Malecha " + "Jakob Botsch Nielsen " + "Matthieu Sozeau " + "Nicolas Tabareau " + "Théo Winterhalter " +] +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" +} diff --git a/extra-dev/packages/coq-metacoq-safechecker-plugin/coq-metacoq-safechecker-plugin.8.17.dev/opam b/extra-dev/packages/coq-metacoq-safechecker-plugin/coq-metacoq-safechecker-plugin.8.17.dev/opam new file mode 100644 index 000000000..d508ae782 --- /dev/null +++ b/extra-dev/packages/coq-metacoq-safechecker-plugin/coq-metacoq-safechecker-plugin.8.17.dev/opam @@ -0,0 +1,47 @@ +opam-version: "2.0" +maintainer: "matthieu.sozeau@inria.fr" +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 " + "Danil Annenkov " + "Simon Boulier " + "Cyril Cohen " + "Yannick Forster " + "Jason Gross " + "Fabian Kunze " + "Meven Lennon-Bertrand " + "Kenji Maillard " + "Gregory Malecha " + "Jakob Botsch Nielsen " + "Matthieu Sozeau " + "Nicolas Tabareau " + "Théo Winterhalter " +] +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" +} diff --git a/extra-dev/packages/coq-metacoq-safechecker/coq-metacoq-safechecker.8.17.dev/opam b/extra-dev/packages/coq-metacoq-safechecker/coq-metacoq-safechecker.8.17.dev/opam new file mode 100644 index 000000000..d2f6f9e5f --- /dev/null +++ b/extra-dev/packages/coq-metacoq-safechecker/coq-metacoq-safechecker.8.17.dev/opam @@ -0,0 +1,41 @@ +opam-version: "2.0" +maintainer: "matthieu.sozeau@inria.fr" +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 " + "Danil Annenkov " + "Simon Boulier " + "Cyril Cohen " + "Yannick Forster " + "Jason Gross " + "Fabian Kunze " + "Meven Lennon-Bertrand " + "Kenji Maillard " + "Gregory Malecha " + "Jakob Botsch Nielsen " + "Matthieu Sozeau " + "Nicolas Tabareau " + "Théo Winterhalter " +] +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" +} diff --git a/extra-dev/packages/coq-metacoq-template-pcuic/coq-metacoq-template-pcuic.8.17.dev/opam b/extra-dev/packages/coq-metacoq-template-pcuic/coq-metacoq-template-pcuic.8.17.dev/opam new file mode 100644 index 000000000..4a0ac65ca --- /dev/null +++ b/extra-dev/packages/coq-metacoq-template-pcuic/coq-metacoq-template-pcuic.8.17.dev/opam @@ -0,0 +1,38 @@ +opam-version: "2.0" +maintainer: "matthieu.sozeau@inria.fr" +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 " + "Danil Annenkov " + "Simon Boulier " + "Cyril Cohen " + "Yannick Forster " + "Jason Gross " + "Fabian Kunze " + "Meven Lennon-Bertrand " + "Kenji Maillard " + "Gregory Malecha " + "Jakob Botsch Nielsen " + "Matthieu Sozeau " + "Nicolas Tabareau " + "Théo Winterhalter " +] +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" +} diff --git a/extra-dev/packages/coq-metacoq-template/coq-metacoq-template.8.17.dev/opam b/extra-dev/packages/coq-metacoq-template/coq-metacoq-template.8.17.dev/opam new file mode 100644 index 000000000..9181754b5 --- /dev/null +++ b/extra-dev/packages/coq-metacoq-template/coq-metacoq-template.8.17.dev/opam @@ -0,0 +1,42 @@ +opam-version: "2.0" +maintainer: "matthieu.sozeau@inria.fr" +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 " + "Danil Annenkov " + "Simon Boulier " + "Cyril Cohen " + "Yannick Forster " + "Jason Gross " + "Fabian Kunze " + "Meven Lennon-Bertrand " + "Kenji Maillard " + "Gregory Malecha " + "Jakob Botsch Nielsen " + "Matthieu Sozeau " + "Nicolas Tabareau " + "Théo Winterhalter " +] +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" +} diff --git a/extra-dev/packages/coq-metacoq-utils/coq-metacoq-utils.8.17.dev/opam b/extra-dev/packages/coq-metacoq-utils/coq-metacoq-utils.8.17.dev/opam new file mode 100644 index 000000000..f2fbec09c --- /dev/null +++ b/extra-dev/packages/coq-metacoq-utils/coq-metacoq-utils.8.17.dev/opam @@ -0,0 +1,40 @@ +opam-version: "2.0" +maintainer: "matthieu.sozeau@inria.fr" +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 " + "Danil Annenkov " + "Simon Boulier " + "Cyril Cohen " + "Yannick Forster " + "Jason Gross " + "Fabian Kunze " + "Meven Lennon-Bertrand " + "Kenji Maillard " + "Gregory Malecha " + "Jakob Botsch Nielsen " + "Matthieu Sozeau " + "Nicolas Tabareau " + "Théo Winterhalter " +] +license: "MIT" +build: [ + ["bash" "./configure.sh"] + [make "-j" "%{jobs}%" "utils"] +] +install: [ + [make "-C" "utils" "install"] +] +depends: [ + "stdlib-shims" + "coq" { >= "8.17" & < "8.18~" } + "coq-equations" { >= "1.3" } +] +synopsis: "The utility 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" +}