[extra-dev] Add rocq-elpi

extra-dev/packages/coq-elpi/coq-elpi.dev/opam

@@ -1,8 +1,6 @@
 # This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
-synopsis: "Elpi extension language for Coq"
-description:
-  "Coq-elpi provides a Coq plugin that embeds ELPI. It also provides a way to embed Coq's terms into λProlog using the Higher-Order Abstract Syntax approach and a way to read terms back. In addition to that it exports to ELPI a set of Coq's primitives, e.g. printing a message, accessing the environment of theorems and data types, defining a new constant and so on. For convenience it also provides a quotation and anti-quotation for Coq's syntax in λProlog. E.g., `{{nat}}` is expanded to the type name of natural numbers, or `{{A -> B}}` to the representation of a product by unfolding the `->` notation. Finally it provides a way to define new vernacular commands and new tactics."
+synopsis: "Compatibility metapackage for Elpi extension language after the Rocq renaming"
 maintainer: ["Enrico Tassi <[email protected]>"]
 authors: ["Enrico Tassi <[email protected]>"]
 license: "LGPL-2.1-or-later"
@@ -15,31 +13,7 @@ tags: [
 homepage: "https://github.com/LPCIC/coq-elpi"
 bug-reports: "https://github.com/LPCIC/coq-elpi/issues"
 depends: [
-  "dune" {>= "3.13"}
-  "ocaml" {>= "4.10.0"}
-  "stdlib-shims"
-  "elpi" {>= "2.0.3" & < "2.1.0~"}
-  "coq" {= "dev"}
-  "ppx_optcomp"
-  "ocaml-lsp-server" {with-dev-setup}
-  "odoc" {with-doc}
-]
-build: [
-  ["dune" "subst"] {dev}
-  [ make "elpi/dune" ]
-  [
-    "dune"
-    "build"
-    "-p"
-    name
-    "-j"
-    jobs
-    "@install"
-    "@runtest" {with-test}
-    "@doc" {with-doc}
-  ]
+  "coq-core"
+  "rocq-elpi" {= version}
 ]
 dev-repo: "git+https://github.com/LPCIC/coq-elpi.git"
-url {
-  src: "git+https://github.com/LPCIC/coq-elpi.git"
-}

extra-dev/packages/rocq-elpi/rocq-elpi.dev/opam

@@ -0,0 +1,47 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+synopsis: "Elpi extension language for Coq"
+description:
+  "Coq-elpi provides a Coq plugin that embeds ELPI. It also provides a way to embed Coq's terms into λProlog using the Higher-Order Abstract Syntax approach and a way to read terms back. In addition to that it exports to ELPI a set of Coq's primitives, e.g. printing a message, accessing the environment of theorems and data types, defining a new constant and so on. For convenience it also provides a quotation and anti-quotation for Coq's syntax in λProlog. E.g., `{{nat}}` is expanded to the type name of natural numbers, or `{{A -> B}}` to the representation of a product by unfolding the `->` notation. Finally it provides a way to define new vernacular commands and new tactics."
+maintainer: ["Enrico Tassi <[email protected]>"]
+authors: ["Enrico Tassi <[email protected]>"]
+license: "LGPL-2.1-or-later"
+tags: [
+  "category:Miscellaneous/Coq Extensions"
+  "keyword:λProlog"
+  "keyword:higher order abstract syntax"
+  "logpath:elpi"
+]
+homepage: "https://github.com/LPCIC/coq-elpi"
+bug-reports: "https://github.com/LPCIC/coq-elpi/issues"
+depends: [
+  "dune" {>= "3.13"}
+  "ocaml" {>= "4.10.0"}
+  "elpi" {>= "2.0.7" & < "2.1.0~"}
+  ("coq" {>= "8.20+rc1" & < "8.21~"}
+  | "rocq-core" {(>= "9.0+rc1" & < "9.1~") | = "dev"})
+  "ppx_optcomp"
+  "ocaml-lsp-server" {with-dev-setup}
+  "odoc" {with-doc}
+  "rocq-stdlib" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [make "dune-files"]
+  [
+    "etc/with-rocq-wrap.sh" {!coq-core:installed}
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
+dev-repo: "git+https://github.com/LPCIC/coq-elpi.git"
+url {
+  src: "git+https://github.com/LPCIC/coq-elpi.git"
+}