Merge pull request #3315 from yforster/coq-metacoq.1.3.3+8.19

Add packages for MetaCoq 1.3.3 on Coq 8.19

released/packages/coq-metacoq-common/coq-metacoq-common.1.3.3+8.19/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/releases/download/v1.3.3-8.19/v1.3.3-8.19.tar.gz"
+  checksum: "sha512=38c27a246201e97249607b1f777eb55ce6e73b273a758a479413ad8110b152e8e0e0a1a2a87206fecbe1079cfd037499c730cdd5adc567a1ef4c7389e71dc337"
+}

released/packages/coq-metacoq-erasure-plugin/coq-metacoq-erasure-plugin.1.3.3+8.19/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/releases/download/v1.3.3-8.19/v1.3.3-8.19.tar.gz"
+  checksum: "sha512=38c27a246201e97249607b1f777eb55ce6e73b273a758a479413ad8110b152e8e0e0a1a2a87206fecbe1079cfd037499c730cdd5adc567a1ef4c7389e71dc337"
+}

released/packages/coq-metacoq-erasure/coq-metacoq-erasure.1.3.3+8.19/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/releases/download/v1.3.3-8.19/v1.3.3-8.19.tar.gz"
+  checksum: "sha512=38c27a246201e97249607b1f777eb55ce6e73b273a758a479413ad8110b152e8e0e0a1a2a87206fecbe1079cfd037499c730cdd5adc567a1ef4c7389e71dc337"
+}

released/packages/coq-metacoq-pcuic/coq-metacoq-pcuic.1.3.3+8.19/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/releases/download/v1.3.3-8.19/v1.3.3-8.19.tar.gz"
+  checksum: "sha512=38c27a246201e97249607b1f777eb55ce6e73b273a758a479413ad8110b152e8e0e0a1a2a87206fecbe1079cfd037499c730cdd5adc567a1ef4c7389e71dc337"
+}

released/packages/coq-metacoq-quotation/coq-metacoq-quotation.1.3.3+8.19/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/releases/download/v1.3.3-8.19/v1.3.3-8.19.tar.gz"
+  checksum: "sha512=38c27a246201e97249607b1f777eb55ce6e73b273a758a479413ad8110b152e8e0e0a1a2a87206fecbe1079cfd037499c730cdd5adc567a1ef4c7389e71dc337"
+}

released/packages/coq-metacoq-safechecker-plugin/coq-metacoq-safechecker-plugin.1.3.3+8.19/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/releases/download/v1.3.3-8.19/v1.3.3-8.19.tar.gz"
+  checksum: "sha512=38c27a246201e97249607b1f777eb55ce6e73b273a758a479413ad8110b152e8e0e0a1a2a87206fecbe1079cfd037499c730cdd5adc567a1ef4c7389e71dc337"
+}

released/packages/coq-metacoq-safechecker/coq-metacoq-safechecker.1.3.3+8.19/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/releases/download/v1.3.3-8.19/v1.3.3-8.19.tar.gz"
+  checksum: "sha512=38c27a246201e97249607b1f777eb55ce6e73b273a758a479413ad8110b152e8e0e0a1a2a87206fecbe1079cfd037499c730cdd5adc567a1ef4c7389e71dc337"
+}

released/packages/coq-metacoq-template-pcuic/coq-metacoq-template-pcuic.1.3.3+8.19/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/releases/download/v1.3.3-8.19/v1.3.3-8.19.tar.gz"
+  checksum: "sha512=38c27a246201e97249607b1f777eb55ce6e73b273a758a479413ad8110b152e8e0e0a1a2a87206fecbe1079cfd037499c730cdd5adc567a1ef4c7389e71dc337"
+}