Add coq-certicoq.dev

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"
+}

extra-dev/packages/coq-metacoq-common/coq-metacoq-common.8.17.dev/opam

@@ -0,0 +1,38 @@
+opam-version: "2.0"
+maintainer: "[email protected]"
+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 <[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: "git+https:///github.com/metacoq/metacoq.git#coq-8.17"
+}

extra-dev/packages/coq-metacoq-erasure-plugin/coq-metacoq-erasure-plugin.8.17.dev/opam

@@ -0,0 +1,47 @@
+opam-version: "2.0"
+maintainer: "[email protected]"
+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 <[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: "git+https:///github.com/metacoq/metacoq.git#coq-8.17"
+}

extra-dev/packages/coq-metacoq-erasure/coq-metacoq-erasure.8.17.dev/opam

@@ -0,0 +1,47 @@
+opam-version: "2.0"
+maintainer: "[email protected]"
+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 <[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: "git+https:///github.com/metacoq/metacoq.git#coq-8.17"
+}

extra-dev/packages/coq-metacoq-pcuic/coq-metacoq-pcuic.8.17.dev/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#coq-8.17"
+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: "git+https:///github.com/metacoq/metacoq.git#coq-8.17"
+}

extra-dev/packages/coq-metacoq-safechecker-plugin/coq-metacoq-safechecker-plugin.8.17.dev/opam

@@ -0,0 +1,47 @@
+opam-version: "2.0"
+maintainer: "[email protected]"
+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 <[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: "git+https:///github.com/metacoq/metacoq.git#coq-8.17"
+}

extra-dev/packages/coq-metacoq-safechecker/coq-metacoq-safechecker.8.17.dev/opam

@@ -0,0 +1,41 @@
+opam-version: "2.0"
+maintainer: "[email protected]"
+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 <[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: "git+https:///github.com/metacoq/metacoq.git#coq-8.17"
+}

extra-dev/packages/coq-metacoq-template-pcuic/coq-metacoq-template-pcuic.8.17.dev/opam

@@ -0,0 +1,38 @@
+opam-version: "2.0"
+maintainer: "[email protected]"
+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 <[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: "git+https:///github.com/metacoq/metacoq.git#coq-8.17"
+}

extra-dev/packages/coq-metacoq-template/coq-metacoq-template.8.17.dev/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#coq-8.17"
+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: "git+https:///github.com/metacoq/metacoq.git#coq-8.17"
+}