[core-dev] Adapt to https://github.com/coq/coq/pull/19530

core-dev/packages/coq-stdlib/coq-stdlib.dev/opam

@@ -13,24 +13,24 @@ formalization of mathematics (e.g. the full formalization of the
 Feit-Thompson theorem or homotopy type theory) and teaching.
 
 This package includes the Coq Standard Library, that is to say, the
-set of modules usually bound to the Coq.* namespace."""
-maintainer: ["The Coq development team <[email protected]>"]
+set of modules usually bound to the Stdlib.* namespace."""
+maintainer: ["The Coq standard library development team"]
 authors: ["The Coq development team, INRIA, CNRS, and contributors"]
 license: "LGPL-2.1-only"
 homepage: "https://coq.inria.fr/"
 doc: "https://coq.github.io/doc/"
 bug-reports: "https://github.com/coq/coq/issues"
 depends: [
-  "dune" {>= "2.9"}
-  "coq-core" {= version}
+  "dune" {>= "3.8"}
+  "coq-core"
+  "rocq-core" {= version}
   "odoc" {with-doc}
 ]
 depopts: ["coq-native"]
 dev-repo: "git+https://github.com/coq/coq.git"
 build: [
+  ["cd" "stdlib"]
   ["dune" "subst"] {dev}
-  # We tell dunestrap to use coq-config from coq-core
-  [ make "dunestrap" "COQ_SPLIT=1" "DUNESTRAPOPT=-p coq-stdlib"]
   [
     "dune"
     "build"
@@ -43,7 +43,7 @@ build: [
     "@runtest" {with-test}
     "@doc" {with-doc}
   ]
-  ["dune" "install" "-p" name "--create-install-files" name]
+  ["dune" "install" "--root" "." "-p" name "--create-install-files" name]
 ]
 
 url {

core-dev/packages/coq/coq.dev/opam

@@ -1,5 +1,5 @@
 opam-version: "2.0"
-synopsis: "The Coq Proof Assistant"
+synopsis: "The Coq Proof Assistant with Stdlib"
 description: """
 Coq is a formal proof management system. It provides
 a formal language to write mathematical definitions, executable
@@ -10,17 +10,20 @@ Typical applications include the certification of properties of
 programming languages (e.g. the CompCert compiler certification
 project, or the Bedrock verified low-level programming library), the
 formalization of mathematics (e.g. the full formalization of the
-Feit-Thompson theorem or homotopy type theory) and teaching."""
+Feit-Thompson theorem or homotopy type theory) and teaching.
+
+This package is a virtual package gathering the rocq-core and coq-stdlib packages."""
 maintainer: ["The Coq development team <[email protected]>"]
 authors: ["The Coq development team, INRIA, CNRS, and contributors"]
 license: "LGPL-2.1-only"
 homepage: "https://coq.inria.fr/"
 doc: "https://coq.github.io/doc/"
 bug-reports: "https://github.com/coq/coq/issues"
 depends: [
-  "dune" {>= "2.9"}
+  "dune" {>= "3.8"}
   "coq-core" {= version}
-  "coq-stdlib" {= version}
+  "rocq-core" {= version}
+  "coq-stdlib"
   "coqide-server" {= version}
   "ounit2" {with-test}
   "odoc" {with-doc}

core-dev/packages/rocq-core/rocq-core.dev/opam

@@ -0,0 +1,52 @@
+opam-version: "2.0"
+synopsis: "The Coq Proof Assistant with its prelude"
+description: """
+Coq is a formal proof management system. It provides
+a formal language to write mathematical definitions, executable
+algorithms and theorems together with an environment for
+semi-interactive development of machine-checked proofs.
+
+Typical applications include the certification of properties of
+programming languages (e.g. the CompCert compiler certification
+project, or the Bedrock verified low-level programming library), the
+formalization of mathematics (e.g. the full formalization of the
+Feit-Thompson theorem or homotopy type theory) and teaching.
+
+This package includes the Rocq prelude, that is loaded automatically
+by Rocq in every .v file, as well as other modules bound to the
+Corelib.* and Ltac2.* namespaces."""
+maintainer: ["The Coq development team <[email protected]>"]
+authors: ["The Coq development team, INRIA, CNRS, and contributors"]
+license: "LGPL-2.1-only"
+homepage: "https://coq.inria.fr/"
+doc: "https://coq.github.io/doc/"
+bug-reports: "https://github.com/coq/coq/issues"
+depends: [
+  "dune" {>= "3.8"}
+  "coq-core" {= version}
+  "odoc" {with-doc}
+]
+depopts: ["coq-native"]
+dev-repo: "git+https://github.com/coq/coq.git"
+build: [
+  ["dune" "subst"] {dev}
+  # We tell dunestrap to use coq-config from coq-core
+  [ make "dunestrap" "COQ_SPLIT=1" "DUNESTRAPOPT=-p rocq-core"]
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "--promote-install-files=false"
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+  ["dune" "install" "-p" name "--create-install-files" name]
+]
+
+url {
+  src: "git+https://github.com/coq/coq.git#master"
+}