From c1c4053106af0dd322a14d0f9f34c5b46ba0196a Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Mon, 23 Dec 2024 20:12:57 +0100
Subject: [PATCH] [core-dev] Rename coq-stdlib -> rocq-stdlib

---
 .../packages/coq-stdlib/coq-stdlib.dev/opam   |  6 +--
 .../packages/rocq-stdlib/rocq-stdlib.dev/opam | 51 +++++++++++++++++++
 2 files changed, 54 insertions(+), 3 deletions(-)
 create mode 100644 core-dev/packages/rocq-stdlib/rocq-stdlib.dev/opam

diff --git a/core-dev/packages/coq-stdlib/coq-stdlib.dev/opam b/core-dev/packages/coq-stdlib/coq-stdlib.dev/opam
index 17da11b1a..b374cde26 100644
--- a/core-dev/packages/coq-stdlib/coq-stdlib.dev/opam
+++ b/core-dev/packages/coq-stdlib/coq-stdlib.dev/opam
@@ -1,5 +1,5 @@
 opam-version: "2.0"
-synopsis: "The Coq Proof Assistant -- Standard Library"
+synopsis: "Compatibility metapackage for Coq Stdlib library after the Rocq renaming"
 description: """
 Coq is a formal proof management system. It provides
 a formal language to write mathematical definitions, executable
@@ -22,8 +22,8 @@ doc: "https://coq.github.io/doc/"
 bug-reports: "https://github.com/coq/coq/issues"
 depends: [
   "dune" {>= "3.8"}
-  "rocq-runtime"
-  "rocq-core" {= version}
+  "coq-core"
+  "rocq-stdlib" {= version}
   "odoc" {with-doc}
 ]
 depopts: ["coq-native"]
diff --git a/core-dev/packages/rocq-stdlib/rocq-stdlib.dev/opam b/core-dev/packages/rocq-stdlib/rocq-stdlib.dev/opam
new file mode 100644
index 000000000..4bfeb6bf4
--- /dev/null
+++ b/core-dev/packages/rocq-stdlib/rocq-stdlib.dev/opam
@@ -0,0 +1,51 @@
+opam-version: "2.0"
+synopsis: "The Rocq Proof Assistant -- Standard Library"
+description: """
+Rocq 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 Standard Library, that is to say, the
+set of modules usually bound to the Stdlib.* namespace."""
+maintainer: ["The Rocq standard library development team"]
+authors: ["The Rocq 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"}
+  "rocq-runtime"
+  "rocq-core" {= version}
+  "odoc" {with-doc}
+]
+depopts: ["coq-native"]
+dev-repo: "git+https://github.com/coq/coq.git"
+build: [
+  ["sh" "-c" "echo '(dirs stdlib)' > dune"]
+  ["dune" "subst"] {dev}
+  [
+    "stdlib/dev/with-rocq-wrap.sh"
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+  ["mv" "stdlib/rocq-stdlib.install" "."]
+]
+
+url {
+  src: "git+https://github.com/coq/coq.git#master"
+}