Add coq-certicoq.dev

and dependencies: - coq-metacoq-erasure-plugin.8.17.dev - coq-metacoq-safechecker-plugin.8.17.dev
coq · Jan 10, 2024 · c05fb93 · c05fb93
1 parent 81998fd
commit c05fb93
Show file tree

Hide file tree

Showing 3 changed files with 139 additions and 0 deletions.
diff --git a/extra-dev/packages/coq-certicoq/coq-certicoq.dev/opam b/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 {
+  git: "https://github.com/CertiCoq/certicoq.git"
+}
diff --git a/extra-dev/packages/coq-metacoq-erasure-plugin/coq-metacoq-erasure-plugin.8.17.dev/opam b/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"
+}
diff --git a/...-dev/packages/coq-metacoq-safechecker-plugin/coq-metacoq-safechecker-plugin.8.17.dev/opam b/...-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"
+}