MetaCoq 1.3.4 for Rocq 9.0

coq · Jan 29, 2025 · 60228d2 · 60228d2
1 parent 3651b6a
commit 60228d2
Show file tree

Hide file tree

Showing 12 changed files with 542 additions and 0 deletions.
diff --git a/extra-dev/packages/coq-metacoq-common/coq-metacoq-common.1.3.4+9.0/opam b/extra-dev/packages/coq-metacoq-common/coq-metacoq-common.1.3.4+9.0/opam
@@ -0,0 +1,39 @@
+opam-version: "2.0"
+maintainer: "matthieu.sozeau@inria.fr"
+homepage: "https://metacoq.github.io/metacoq"
+dev-repo: "git+https://github.com/MetaCoq/metacoq.git#main"
+bug-reports: "https://github.com/MetaCoq/metacoq/issues"
+authors: ["Abhishek Anand <aa755@cs.cornell.edu>"
+          "Danil Annenkov <danil.v.annenkov@gmail.com>"
+          "Simon Boulier <simon.boulier@inria.fr>"
+          "Cyril Cohen <cyril.cohen@inria.fr>"
+          "Yannick Forster <forster@ps.uni-saarland.de>"
+          "Jason Gross <jgross@mit.edu>"
+          "Fabian Kunze <fkunze@fakusb.de>"
+          "Meven Lennon-Bertrand <Meven.Bertrand@univ-nantes.fr>"
+          "Kenji Maillard <kenji.maillard@inria.fr>"
+          "Gregory Malecha <gmalecha@gmail.com>"
+          "Jakob Botsch Nielsen <Jakob.botsch.nielsen@gmail.com>"
+          "Matthieu Sozeau <matthieu.sozeau@inria.fr>"
+          "Nicolas Tabareau <nicolas.tabareau@inria.fr>"
+          "Théo Winterhalter <theo.winterhalter@inria.fr>"
+]
+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: "https://github.com/MetaCoq/metacoq/releases/download/v1.3.4-9.0/v1.3.4-9.0.tar.gz"
+  checksum: "sha512=0243145ea97a99532da856b28b1bdd99f7db083cddfd04855b3b298611b894f6e14aa0628f0a236e9893a5a69f1a82b8af94ed6ea5b5a401fd55f6336230a8d8"
+}
diff --git a/extra-dev/packages/coq-metacoq-erasure-plugin/coq-metacoq-erasure-plugin.1.3.4+9.0/opam b/extra-dev/packages/coq-metacoq-erasure-plugin/coq-metacoq-erasure-plugin.1.3.4+9.0/opam
@@ -0,0 +1,48 @@
+opam-version: "2.0"
+maintainer: "matthieu.sozeau@inria.fr"
+homepage: "https://metacoq.github.io/metacoq"
+dev-repo: "git+https://github.com/MetaCoq/metacoq.git#main"
+bug-reports: "https://github.com/MetaCoq/metacoq/issues"
+authors: ["Abhishek Anand <aa755@cs.cornell.edu>"
+          "Danil Annenkov <danil.v.annenkov@gmail.com>"
+          "Simon Boulier <simon.boulier@inria.fr>"
+          "Cyril Cohen <cyril.cohen@inria.fr>"
+          "Yannick Forster <forster@ps.uni-saarland.de>"
+          "Jason Gross <jgross@mit.edu>"
+          "Fabian Kunze <fkunze@fakusb.de>"
+          "Meven Lennon-Bertrand <Meven.Bertrand@univ-nantes.fr>"
+          "Kenji Maillard <kenji.maillard@inria.fr>"
+          "Gregory Malecha <gmalecha@gmail.com>"
+          "Jakob Botsch Nielsen <Jakob.botsch.nielsen@gmail.com>"
+          "Matthieu Sozeau <matthieu.sozeau@inria.fr>"
+          "Nicolas Tabareau <nicolas.tabareau@inria.fr>"
+          "Théo Winterhalter <theo.winterhalter@inria.fr>"
+]
+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: "https://github.com/MetaCoq/metacoq/releases/download/v1.3.4-9.0/v1.3.4-9.0.tar.gz"
+  checksum: "sha512=0243145ea97a99532da856b28b1bdd99f7db083cddfd04855b3b298611b894f6e14aa0628f0a236e9893a5a69f1a82b8af94ed6ea5b5a401fd55f6336230a8d8"
+}
diff --git a/extra-dev/packages/coq-metacoq-erasure/coq-metacoq-erasure.1.3.4+9.0/opam b/extra-dev/packages/coq-metacoq-erasure/coq-metacoq-erasure.1.3.4+9.0/opam
@@ -0,0 +1,48 @@
+opam-version: "2.0"
+maintainer: "matthieu.sozeau@inria.fr"
+homepage: "https://metacoq.github.io/metacoq"
+dev-repo: "git+https://github.com/MetaCoq/metacoq.git#main"
+bug-reports: "https://github.com/MetaCoq/metacoq/issues"
+authors: ["Abhishek Anand <aa755@cs.cornell.edu>"
+          "Danil Annenkov <danil.v.annenkov@gmail.com>"
+          "Simon Boulier <simon.boulier@inria.fr>"
+          "Cyril Cohen <cyril.cohen@inria.fr>"
+          "Yannick Forster <forster@ps.uni-saarland.de>"
+          "Jason Gross <jgross@mit.edu>"
+          "Fabian Kunze <fkunze@fakusb.de>"
+          "Meven Lennon-Bertrand <Meven.Bertrand@univ-nantes.fr>"
+          "Kenji Maillard <kenji.maillard@inria.fr>"
+          "Gregory Malecha <gmalecha@gmail.com>"
+          "Jakob Botsch Nielsen <Jakob.botsch.nielsen@gmail.com>"
+          "Matthieu Sozeau <matthieu.sozeau@inria.fr>"
+          "Nicolas Tabareau <nicolas.tabareau@inria.fr>"
+          "Théo Winterhalter <theo.winterhalter@inria.fr>"
+]
+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: "https://github.com/MetaCoq/metacoq/releases/download/v1.3.4-9.0/v1.3.4-9.0.tar.gz"
+  checksum: "sha512=0243145ea97a99532da856b28b1bdd99f7db083cddfd04855b3b298611b894f6e14aa0628f0a236e9893a5a69f1a82b8af94ed6ea5b5a401fd55f6336230a8d8"
+}
diff --git a/extra-dev/packages/coq-metacoq-pcuic/coq-metacoq-pcuic.1.3.4+9.0/opam b/extra-dev/packages/coq-metacoq-pcuic/coq-metacoq-pcuic.1.3.4+9.0/opam
@@ -0,0 +1,43 @@
+opam-version: "2.0"
+maintainer: "matthieu.sozeau@inria.fr"
+homepage: "https://metacoq.github.io/metacoq"
+dev-repo: "git+https://github.com/MetaCoq/metacoq.git#main"
+bug-reports: "https://github.com/MetaCoq/metacoq/issues"
+authors: ["Abhishek Anand <aa755@cs.cornell.edu>"
+          "Danil Annenkov <danil.v.annenkov@gmail.com>"
+          "Simon Boulier <simon.boulier@inria.fr>"
+          "Cyril Cohen <cyril.cohen@inria.fr>"
+          "Yannick Forster <forster@ps.uni-saarland.de>"
+          "Jason Gross <jgross@mit.edu>"
+          "Fabian Kunze <fkunze@fakusb.de>"
+          "Meven Lennon-Bertrand <Meven.Bertrand@univ-nantes.fr>"
+          "Kenji Maillard <kenji.maillard@inria.fr>"
+          "Gregory Malecha <gmalecha@gmail.com>"
+          "Jakob Botsch Nielsen <Jakob.botsch.nielsen@gmail.com>"
+          "Matthieu Sozeau <matthieu.sozeau@inria.fr>"
+          "Nicolas Tabareau <nicolas.tabareau@inria.fr>"
+          "Théo Winterhalter <theo.winterhalter@inria.fr>"
+]
+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: "https://github.com/MetaCoq/metacoq/releases/download/v1.3.4-9.0/v1.3.4-9.0.tar.gz"
+  checksum: "sha512=0243145ea97a99532da856b28b1bdd99f7db083cddfd04855b3b298611b894f6e14aa0628f0a236e9893a5a69f1a82b8af94ed6ea5b5a401fd55f6336230a8d8"
+}
diff --git a/extra-dev/packages/coq-metacoq-quotation/coq-metacoq-quotation.1.3.4+9.0/opam b/extra-dev/packages/coq-metacoq-quotation/coq-metacoq-quotation.1.3.4+9.0/opam
@@ -0,0 +1,53 @@
+opam-version: "2.0"
+maintainer: "matthieu.sozeau@inria.fr"
+homepage: "https://metacoq.github.io/metacoq"
+dev-repo: "git+https://github.com/MetaCoq/metacoq.git#main"
+bug-reports: "https://github.com/MetaCoq/metacoq/issues"
+authors: ["Abhishek Anand <aa755@cs.cornell.edu>"
+          "Danil Annenkov <danil.v.annenkov@gmail.com>"
+          "Simon Boulier <simon.boulier@inria.fr>"
+          "Cyril Cohen <cyril.cohen@inria.fr>"
+          "Yannick Forster <forster@ps.uni-saarland.de>"
+          "Jason Gross <jgross@mit.edu>"
+          "Fabian Kunze <fkunze@fakusb.de>"
+          "Meven Lennon-Bertrand <Meven.Bertrand@univ-nantes.fr>"
+          "Kenji Maillard <kenji.maillard@inria.fr>"
+          "Gregory Malecha <gmalecha@gmail.com>"
+          "Jakob Botsch Nielsen <Jakob.botsch.nielsen@gmail.com>"
+          "Matthieu Sozeau <matthieu.sozeau@inria.fr>"
+          "Nicolas Tabareau <nicolas.tabareau@inria.fr>"
+          "Théo Winterhalter <theo.winterhalter@inria.fr>"
+]
+license: "MIT"
+build: [
+  ["bash" "./configure.sh"]
+  [make "-j" "%{jobs}%" "-C" "quotation"]
+]
+install: [
+  [make "-C" "quotation" "install"]
+]
+depends: [
+  "coq-metacoq-template" {= version}
+  "coq-metacoq-pcuic" {= version}
+  "coq-metacoq-template-pcuic" {= version}
+]
+synopsis: "Gallina quotation functions for Template Coq"
+description: """
+MetaCoq is a meta-programming framework for Coq.
+
+The Quotation module is geared at providing functions `□T → □□T` for
+`□T := Ast.term` (currently implemented) and for `□T := { t : Ast.term
+& Σ ;;; [] |- t : T }` (still in the works).  Currently `Ast.term →
+Ast.term` and `(Σ ;;; [] |- t : T) → Ast.term` functions are provided
+for Template and PCUIC terms, in `MetaCoq.Quotation.ToTemplate.All`
+and `MetaCoq.Quotation.ToPCUIC.All`.  Proving well-typedness is still
+a work in progress.
+
+Ultimately the goal of this development is to prove that `□` is a lax monoidal
+semicomonad (a functor with `cojoin : □T → □□T` that codistributes over `unit`
+and `×`), which is sufficient for proving Löb's theorem.
+"""
+url {
+  src: "https://github.com/MetaCoq/metacoq/releases/download/v1.3.4-9.0/v1.3.4-9.0.tar.gz"
+  checksum: "sha512=0243145ea97a99532da856b28b1bdd99f7db083cddfd04855b3b298611b894f6e14aa0628f0a236e9893a5a69f1a82b8af94ed6ea5b5a401fd55f6336230a8d8"
+}
diff --git a/...dev/packages/coq-metacoq-safechecker-plugin/coq-metacoq-safechecker-plugin.1.3.4+9.0/opam b/...dev/packages/coq-metacoq-safechecker-plugin/coq-metacoq-safechecker-plugin.1.3.4+9.0/opam
@@ -0,0 +1,48 @@
+opam-version: "2.0"
+maintainer: "matthieu.sozeau@inria.fr"
+homepage: "https://metacoq.github.io/metacoq"
+dev-repo: "git+https://github.com/MetaCoq/metacoq.git#main"
+bug-reports: "https://github.com/MetaCoq/metacoq/issues"
+authors: ["Abhishek Anand <aa755@cs.cornell.edu>"
+          "Danil Annenkov <danil.v.annenkov@gmail.com>"
+          "Simon Boulier <simon.boulier@inria.fr>"
+          "Cyril Cohen <cyril.cohen@inria.fr>"
+          "Yannick Forster <forster@ps.uni-saarland.de>"
+          "Jason Gross <jgross@mit.edu>"
+          "Fabian Kunze <fkunze@fakusb.de>"
+          "Meven Lennon-Bertrand <Meven.Bertrand@univ-nantes.fr>"
+          "Kenji Maillard <kenji.maillard@inria.fr>"
+          "Gregory Malecha <gmalecha@gmail.com>"
+          "Jakob Botsch Nielsen <Jakob.botsch.nielsen@gmail.com>"
+          "Matthieu Sozeau <matthieu.sozeau@inria.fr>"
+          "Nicolas Tabareau <nicolas.tabareau@inria.fr>"
+          "Théo Winterhalter <theo.winterhalter@inria.fr>"
+]
+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: "https://github.com/MetaCoq/metacoq/releases/download/v1.3.4-9.0/v1.3.4-9.0.tar.gz"
+  checksum: "sha512=0243145ea97a99532da856b28b1bdd99f7db083cddfd04855b3b298611b894f6e14aa0628f0a236e9893a5a69f1a82b8af94ed6ea5b5a401fd55f6336230a8d8"
+}
diff --git a/extra-dev/packages/coq-metacoq-safechecker/coq-metacoq-safechecker.1.3.4+9.0/opam b/extra-dev/packages/coq-metacoq-safechecker/coq-metacoq-safechecker.1.3.4+9.0/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#main"
+bug-reports: "https://github.com/MetaCoq/metacoq/issues"
+authors: ["Abhishek Anand <aa755@cs.cornell.edu>"
+          "Danil Annenkov <danil.v.annenkov@gmail.com>"
+          "Simon Boulier <simon.boulier@inria.fr>"
+          "Cyril Cohen <cyril.cohen@inria.fr>"
+          "Yannick Forster <forster@ps.uni-saarland.de>"
+          "Jason Gross <jgross@mit.edu>"
+          "Fabian Kunze <fkunze@fakusb.de>"
+          "Meven Lennon-Bertrand <Meven.Bertrand@univ-nantes.fr>"
+          "Kenji Maillard <kenji.maillard@inria.fr>"
+          "Gregory Malecha <gmalecha@gmail.com>"
+          "Jakob Botsch Nielsen <Jakob.botsch.nielsen@gmail.com>"
+          "Matthieu Sozeau <matthieu.sozeau@inria.fr>"
+          "Nicolas Tabareau <nicolas.tabareau@inria.fr>"
+          "Théo Winterhalter <theo.winterhalter@inria.fr>"
+]
+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: "https://github.com/MetaCoq/metacoq/releases/download/v1.3.4-9.0/v1.3.4-9.0.tar.gz"
+  checksum: "sha512=0243145ea97a99532da856b28b1bdd99f7db083cddfd04855b3b298611b894f6e14aa0628f0a236e9893a5a69f1a82b8af94ed6ea5b5a401fd55f6336230a8d8"
+}
diff --git a/extra-dev/packages/coq-metacoq-template-pcuic/coq-metacoq-template-pcuic.1.3.4+9.0/opam b/extra-dev/packages/coq-metacoq-template-pcuic/coq-metacoq-template-pcuic.1.3.4+9.0/opam
@@ -0,0 +1,39 @@
+opam-version: "2.0"
+maintainer: "matthieu.sozeau@inria.fr"
+homepage: "https://metacoq.github.io/metacoq"
+dev-repo: "git+https://github.com/MetaCoq/metacoq.git#main"
+bug-reports: "https://github.com/MetaCoq/metacoq/issues"
+authors: ["Abhishek Anand <aa755@cs.cornell.edu>"
+          "Danil Annenkov <danil.v.annenkov@gmail.com>"
+          "Simon Boulier <simon.boulier@inria.fr>"
+          "Cyril Cohen <cyril.cohen@inria.fr>"
+          "Yannick Forster <forster@ps.uni-saarland.de>"
+          "Jason Gross <jgross@mit.edu>"
+          "Fabian Kunze <fkunze@fakusb.de>"
+          "Meven Lennon-Bertrand <Meven.Bertrand@univ-nantes.fr>"
+          "Kenji Maillard <kenji.maillard@inria.fr>"
+          "Gregory Malecha <gmalecha@gmail.com>"
+          "Jakob Botsch Nielsen <Jakob.botsch.nielsen@gmail.com>"
+          "Matthieu Sozeau <matthieu.sozeau@inria.fr>"
+          "Nicolas Tabareau <nicolas.tabareau@inria.fr>"
+          "Théo Winterhalter <theo.winterhalter@inria.fr>"
+]
+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: "https://github.com/MetaCoq/metacoq/releases/download/v1.3.4-9.0/v1.3.4-9.0.tar.gz"
+  checksum: "sha512=0243145ea97a99532da856b28b1bdd99f7db083cddfd04855b3b298611b894f6e14aa0628f0a236e9893a5a69f1a82b8af94ed6ea5b5a401fd55f6336230a8d8"
+}