Merge pull request #3316 from yforster/coq-metacoq.1.3.4+8.20

Add packages for MetaCoq 1.3.4 on Coq 8.20
coq · Jan 28, 2025 · 7ee1240 · 7ee1240
2 parents e6989c8 + 2bd8bbe
commit 7ee1240
Show file tree

Hide file tree

Showing 12 changed files with 541 additions and 0 deletions.
diff --git a/released/packages/coq-metacoq-common/coq-metacoq-common.1.3.4+8.20/opam b/released/packages/coq-metacoq-common/coq-metacoq-common.1.3.4+8.20/opam
@@ -0,0 +1,39 @@
+opam-version: "2.0"
+maintainer: "[email protected]"
+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 <[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: "https://github.com/MetaCoq/metacoq/archive/refs/tags/v1.3.4-8.20.tar.gz"
+  checksum: "sha512=fb3997e2e07e9c33c293aabcc06b8e69785a9c2ebdcd4d48f77e1eb09698da6ed1770127022843f89322cf8f78289acd67c860e1a2d9186d5703191ccd088429"
+}
diff --git a/released/packages/coq-metacoq-erasure-plugin/coq-metacoq-erasure-plugin.1.3.4+8.20/opam b/released/packages/coq-metacoq-erasure-plugin/coq-metacoq-erasure-plugin.1.3.4+8.20/opam
@@ -0,0 +1,48 @@
+opam-version: "2.0"
+maintainer: "[email protected]"
+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 <[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: "https://github.com/MetaCoq/metacoq/archive/refs/tags/v1.3.4-8.20.tar.gz"
+  checksum: "sha512=fb3997e2e07e9c33c293aabcc06b8e69785a9c2ebdcd4d48f77e1eb09698da6ed1770127022843f89322cf8f78289acd67c860e1a2d9186d5703191ccd088429"
+}
diff --git a/released/packages/coq-metacoq-erasure/coq-metacoq-erasure.1.3.4+8.20/opam b/released/packages/coq-metacoq-erasure/coq-metacoq-erasure.1.3.4+8.20/opam
@@ -0,0 +1,48 @@
+opam-version: "2.0"
+maintainer: "[email protected]"
+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 <[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: "https://github.com/MetaCoq/metacoq/archive/refs/tags/v1.3.4-8.20.tar.gz"
+  checksum: "sha512=fb3997e2e07e9c33c293aabcc06b8e69785a9c2ebdcd4d48f77e1eb09698da6ed1770127022843f89322cf8f78289acd67c860e1a2d9186d5703191ccd088429"
+}
diff --git a/released/packages/coq-metacoq-pcuic/coq-metacoq-pcuic.1.3.4+8.20/opam b/released/packages/coq-metacoq-pcuic/coq-metacoq-pcuic.1.3.4+8.20/opam
@@ -0,0 +1,43 @@
+opam-version: "2.0"
+maintainer: "[email protected]"
+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 <[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: "https://github.com/MetaCoq/metacoq/archive/refs/tags/v1.3.4-8.20.tar.gz"
+  checksum: "sha512=fb3997e2e07e9c33c293aabcc06b8e69785a9c2ebdcd4d48f77e1eb09698da6ed1770127022843f89322cf8f78289acd67c860e1a2d9186d5703191ccd088429"
+}
diff --git a/released/packages/coq-metacoq-quotation/coq-metacoq-quotation.1.3.4+8.20/opam b/released/packages/coq-metacoq-quotation/coq-metacoq-quotation.1.3.4+8.20/opam
@@ -0,0 +1,53 @@
+opam-version: "2.0"
+maintainer: "[email protected]"
+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 <[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" "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/archive/refs/tags/v1.3.4-8.20.tar.gz"
+  checksum: "sha512=fb3997e2e07e9c33c293aabcc06b8e69785a9c2ebdcd4d48f77e1eb09698da6ed1770127022843f89322cf8f78289acd67c860e1a2d9186d5703191ccd088429"
+}
diff --git a/...ed/packages/coq-metacoq-safechecker-plugin/coq-metacoq-safechecker-plugin.1.3.4+8.20/opam b/...ed/packages/coq-metacoq-safechecker-plugin/coq-metacoq-safechecker-plugin.1.3.4+8.20/opam
@@ -0,0 +1,48 @@
+opam-version: "2.0"
+maintainer: "[email protected]"
+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 <[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: "https://github.com/MetaCoq/metacoq/archive/refs/tags/v1.3.4-8.20.tar.gz"
+  checksum: "sha512=fb3997e2e07e9c33c293aabcc06b8e69785a9c2ebdcd4d48f77e1eb09698da6ed1770127022843f89322cf8f78289acd67c860e1a2d9186d5703191ccd088429"
+}
diff --git a/released/packages/coq-metacoq-safechecker/coq-metacoq-safechecker.1.3.4+8.20/opam b/released/packages/coq-metacoq-safechecker/coq-metacoq-safechecker.1.3.4+8.20/opam
@@ -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#main"
+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: "https://github.com/MetaCoq/metacoq/archive/refs/tags/v1.3.4-8.20.tar.gz"
+  checksum: "sha512=fb3997e2e07e9c33c293aabcc06b8e69785a9c2ebdcd4d48f77e1eb09698da6ed1770127022843f89322cf8f78289acd67c860e1a2d9186d5703191ccd088429"
+}
diff --git a/released/packages/coq-metacoq-template-pcuic/coq-metacoq-template-pcuic.1.3.4+8.20/opam b/released/packages/coq-metacoq-template-pcuic/coq-metacoq-template-pcuic.1.3.4+8.20/opam
@@ -0,0 +1,39 @@
+opam-version: "2.0"
+maintainer: "[email protected]"
+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 <[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: "https://github.com/MetaCoq/metacoq/archive/refs/tags/v1.3.4-8.20.tar.gz"
+  checksum: "sha512=fb3997e2e07e9c33c293aabcc06b8e69785a9c2ebdcd4d48f77e1eb09698da6ed1770127022843f89322cf8f78289acd67c860e1a2d9186d5703191ccd088429"
+}