From 6405f65bc2b6cbcb6c7e10a263c72cf9d9ad3848 Mon Sep 17 00:00:00 2001 From: Yannick Forster Date: Mon, 27 Jan 2025 13:17:21 +0100 Subject: [PATCH] Add packages for MetaCoq 1.3.3 on Coq 8.19 --- .../coq-metacoq-common.1.3.3+8.19/opam | 39 ++++++++++++++ .../opam | 48 +++++++++++++++++ .../coq-metacoq-erasure.1.3.3+8.19/opam | 48 +++++++++++++++++ .../coq-metacoq-pcuic.1.3.3+8.19/opam | 43 +++++++++++++++ .../coq-metacoq-quotation.1.3.3+8.19/opam | 53 +++++++++++++++++++ .../opam | 48 +++++++++++++++++ .../coq-metacoq-safechecker.1.3.3+8.19/opam | 42 +++++++++++++++ .../opam | 39 ++++++++++++++ .../coq-metacoq-template.1.3.3+8.19/opam | 52 ++++++++++++++++++ .../coq-metacoq-translations.1.3.3+8.19/opam | 43 +++++++++++++++ .../coq-metacoq-utils.1.3.3+8.19/opam | 41 ++++++++++++++ .../coq-metacoq/coq-metacoq.1.3.3+8.19/opam | 46 ++++++++++++++++ 12 files changed, 542 insertions(+) create mode 100644 released/packages/coq-metacoq-common/coq-metacoq-common.1.3.3+8.19/opam create mode 100644 released/packages/coq-metacoq-erasure-plugin/coq-metacoq-erasure-plugin.1.3.3+8.19/opam create mode 100644 released/packages/coq-metacoq-erasure/coq-metacoq-erasure.1.3.3+8.19/opam create mode 100644 released/packages/coq-metacoq-pcuic/coq-metacoq-pcuic.1.3.3+8.19/opam create mode 100644 released/packages/coq-metacoq-quotation/coq-metacoq-quotation.1.3.3+8.19/opam create mode 100644 released/packages/coq-metacoq-safechecker-plugin/coq-metacoq-safechecker-plugin.1.3.3+8.19/opam create mode 100644 released/packages/coq-metacoq-safechecker/coq-metacoq-safechecker.1.3.3+8.19/opam create mode 100644 released/packages/coq-metacoq-template-pcuic/coq-metacoq-template-pcuic.1.3.3+8.19/opam create mode 100644 released/packages/coq-metacoq-template/coq-metacoq-template.1.3.3+8.19/opam create mode 100644 released/packages/coq-metacoq-translations/coq-metacoq-translations.1.3.3+8.19/opam create mode 100644 released/packages/coq-metacoq-utils/coq-metacoq-utils.1.3.3+8.19/opam create mode 100644 released/packages/coq-metacoq/coq-metacoq.1.3.3+8.19/opam diff --git a/released/packages/coq-metacoq-common/coq-metacoq-common.1.3.3+8.19/opam b/released/packages/coq-metacoq-common/coq-metacoq-common.1.3.3+8.19/opam new file mode 100644 index 0000000000..ee17cf5714 --- /dev/null +++ b/released/packages/coq-metacoq-common/coq-metacoq-common.1.3.3+8.19/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 " + "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: "https://github.com/MetaCoq/metacoq/releases/download/v1.3.3-8.19/v1.3.3-8.19.tar.gz" + checksum: "sha512=38c27a246201e97249607b1f777eb55ce6e73b273a758a479413ad8110b152e8e0e0a1a2a87206fecbe1079cfd037499c730cdd5adc567a1ef4c7389e71dc337" +} diff --git a/released/packages/coq-metacoq-erasure-plugin/coq-metacoq-erasure-plugin.1.3.3+8.19/opam b/released/packages/coq-metacoq-erasure-plugin/coq-metacoq-erasure-plugin.1.3.3+8.19/opam new file mode 100644 index 0000000000..6c22fc10f3 --- /dev/null +++ b/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: "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 " + "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: "https://github.com/MetaCoq/metacoq/releases/download/v1.3.3-8.19/v1.3.3-8.19.tar.gz" + checksum: "sha512=38c27a246201e97249607b1f777eb55ce6e73b273a758a479413ad8110b152e8e0e0a1a2a87206fecbe1079cfd037499c730cdd5adc567a1ef4c7389e71dc337" +} diff --git a/released/packages/coq-metacoq-erasure/coq-metacoq-erasure.1.3.3+8.19/opam b/released/packages/coq-metacoq-erasure/coq-metacoq-erasure.1.3.3+8.19/opam new file mode 100644 index 0000000000..0944a71cd0 --- /dev/null +++ b/released/packages/coq-metacoq-erasure/coq-metacoq-erasure.1.3.3+8.19/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 " + "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: "https://github.com/MetaCoq/metacoq/releases/download/v1.3.3-8.19/v1.3.3-8.19.tar.gz" + checksum: "sha512=38c27a246201e97249607b1f777eb55ce6e73b273a758a479413ad8110b152e8e0e0a1a2a87206fecbe1079cfd037499c730cdd5adc567a1ef4c7389e71dc337" +} diff --git a/released/packages/coq-metacoq-pcuic/coq-metacoq-pcuic.1.3.3+8.19/opam b/released/packages/coq-metacoq-pcuic/coq-metacoq-pcuic.1.3.3+8.19/opam new file mode 100644 index 0000000000..dcffdde0e5 --- /dev/null +++ b/released/packages/coq-metacoq-pcuic/coq-metacoq-pcuic.1.3.3+8.19/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 " + "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: "https://github.com/MetaCoq/metacoq/releases/download/v1.3.3-8.19/v1.3.3-8.19.tar.gz" + checksum: "sha512=38c27a246201e97249607b1f777eb55ce6e73b273a758a479413ad8110b152e8e0e0a1a2a87206fecbe1079cfd037499c730cdd5adc567a1ef4c7389e71dc337" +} diff --git a/released/packages/coq-metacoq-quotation/coq-metacoq-quotation.1.3.3+8.19/opam b/released/packages/coq-metacoq-quotation/coq-metacoq-quotation.1.3.3+8.19/opam new file mode 100644 index 0000000000..3ef8911d41 --- /dev/null +++ b/released/packages/coq-metacoq-quotation/coq-metacoq-quotation.1.3.3+8.19/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 " + "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" "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" +} diff --git a/released/packages/coq-metacoq-safechecker-plugin/coq-metacoq-safechecker-plugin.1.3.3+8.19/opam b/released/packages/coq-metacoq-safechecker-plugin/coq-metacoq-safechecker-plugin.1.3.3+8.19/opam new file mode 100644 index 0000000000..67d58c401f --- /dev/null +++ b/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: "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 " + "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: "https://github.com/MetaCoq/metacoq/releases/download/v1.3.3-8.19/v1.3.3-8.19.tar.gz" + checksum: "sha512=38c27a246201e97249607b1f777eb55ce6e73b273a758a479413ad8110b152e8e0e0a1a2a87206fecbe1079cfd037499c730cdd5adc567a1ef4c7389e71dc337" +} diff --git a/released/packages/coq-metacoq-safechecker/coq-metacoq-safechecker.1.3.3+8.19/opam b/released/packages/coq-metacoq-safechecker/coq-metacoq-safechecker.1.3.3+8.19/opam new file mode 100644 index 0000000000..7ad9aebede --- /dev/null +++ b/released/packages/coq-metacoq-safechecker/coq-metacoq-safechecker.1.3.3+8.19/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 " + "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: "https://github.com/MetaCoq/metacoq/releases/download/v1.3.3-8.19/v1.3.3-8.19.tar.gz" + checksum: "sha512=38c27a246201e97249607b1f777eb55ce6e73b273a758a479413ad8110b152e8e0e0a1a2a87206fecbe1079cfd037499c730cdd5adc567a1ef4c7389e71dc337" +} diff --git a/released/packages/coq-metacoq-template-pcuic/coq-metacoq-template-pcuic.1.3.3+8.19/opam b/released/packages/coq-metacoq-template-pcuic/coq-metacoq-template-pcuic.1.3.3+8.19/opam new file mode 100644 index 0000000000..35900c5b16 --- /dev/null +++ b/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: "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 " + "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: "https://github.com/MetaCoq/metacoq/releases/download/v1.3.3-8.19/v1.3.3-8.19.tar.gz" + checksum: "sha512=38c27a246201e97249607b1f777eb55ce6e73b273a758a479413ad8110b152e8e0e0a1a2a87206fecbe1079cfd037499c730cdd5adc567a1ef4c7389e71dc337" +} diff --git a/released/packages/coq-metacoq-template/coq-metacoq-template.1.3.3+8.19/opam b/released/packages/coq-metacoq-template/coq-metacoq-template.1.3.3+8.19/opam new file mode 100644 index 0000000000..53f724d557 --- /dev/null +++ b/released/packages/coq-metacoq-template/coq-metacoq-template.1.3.3+8.19/opam @@ -0,0 +1,52 @@ +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 " + "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-coq"] +] +install: [ + [make "-C" "template-coq" "install"] +] +depends: [ + "coq-metacoq-common" {= version} +] +synopsis: "A quoting and unquoting library for Coq in Coq" +description: """ +MetaCoq is a meta-programming framework for Coq. + +Template Coq is a quoting library for Coq. It takes Coq terms and +constructs a representation of their syntax tree as a Coq inductive data +type. The representation is based on the kernel's term representation. + +In addition to a complete reification and denotation of CIC terms, +Template Coq includes: + +- Reification of the environment structures, for constant and inductive declarations. +- Denotation of terms and global declarations +- A monad for manipulating global declarations, calling the type + checker, and inserting them in the global environment, in the style of + MetaCoq/MTac. +""" +url { + src: "https://github.com/MetaCoq/metacoq/releases/download/v1.3.3-8.19/v1.3.3-8.19.tar.gz" + checksum: "sha512=38c27a246201e97249607b1f777eb55ce6e73b273a758a479413ad8110b152e8e0e0a1a2a87206fecbe1079cfd037499c730cdd5adc567a1ef4c7389e71dc337" +} diff --git a/released/packages/coq-metacoq-translations/coq-metacoq-translations.1.3.3+8.19/opam b/released/packages/coq-metacoq-translations/coq-metacoq-translations.1.3.3+8.19/opam new file mode 100644 index 0000000000..27f1f94177 --- /dev/null +++ b/released/packages/coq-metacoq-translations/coq-metacoq-translations.1.3.3+8.19/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 " + "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" "translations"] +] +install: [ + [make "-C" "translations" "install"] +] +depends: [ + "coq-metacoq-template" {= version} +] +synopsis: "Translations built on top of MetaCoq" +description: """ +MetaCoq is a meta-programming framework for Coq. + +The Translations modules provides implementation of standard translations +from type theory to type theory, e.g. parametricity and the `cross-bool` +translation that invalidates functional extensionality. +""" +url { + src: "https://github.com/MetaCoq/metacoq/releases/download/v1.3.3-8.19/v1.3.3-8.19.tar.gz" + checksum: "sha512=38c27a246201e97249607b1f777eb55ce6e73b273a758a479413ad8110b152e8e0e0a1a2a87206fecbe1079cfd037499c730cdd5adc567a1ef4c7389e71dc337" +} diff --git a/released/packages/coq-metacoq-utils/coq-metacoq-utils.1.3.3+8.19/opam b/released/packages/coq-metacoq-utils/coq-metacoq-utils.1.3.3+8.19/opam new file mode 100644 index 0000000000..3cf6d910ca --- /dev/null +++ b/released/packages/coq-metacoq-utils/coq-metacoq-utils.1.3.3+8.19/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#main" +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.19" & < "8.20~" } + "coq-equations" { = "1.3+8.19" } +] +synopsis: "The utility 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" +} diff --git a/released/packages/coq-metacoq/coq-metacoq.1.3.3+8.19/opam b/released/packages/coq-metacoq/coq-metacoq.1.3.3+8.19/opam new file mode 100644 index 0000000000..065c344af7 --- /dev/null +++ b/released/packages/coq-metacoq/coq-metacoq.1.3.3+8.19/opam @@ -0,0 +1,46 @@ +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 " + "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" +depends: [ + "coq-metacoq-safechecker-plugin" {= version} + "coq-metacoq-erasure-plugin" {= version} + "coq-metacoq-translations" {= version} + "coq-metacoq-quotation" {= version} +] +build: [ + ["bash" "./configure.sh" ] {with-test} + [make "-C" "examples" ] {with-test} + [make "-C" "test-suite" ] {with-test} +] +synopsis: "A meta-programming framework for Coq" +description: """ +MetaCoq is a meta-programming framework for Coq. + +The meta-package includes the template-coq library, +the PCUIC development including a verified equivalence between Coq and PCUIC, +a safe type checker and verified erasure for PCUIC and example translations. + +See individual packages for more detailed descriptions. +""" +url { + src: "https://github.com/MetaCoq/metacoq/releases/download/v1.3.3-8.19/v1.3.3-8.19.tar.gz" + checksum: "sha512=38c27a246201e97249607b1f777eb55ce6e73b273a758a479413ad8110b152e8e0e0a1a2a87206fecbe1079cfd037499c730cdd5adc567a1ef4c7389e71dc337" +}