more 9.0.dev fixes

[palmskog]

@silene can you double check and please merge if all required changes are there now?

For example, I wasn't even aware that that the rocq-native metapackage would be changed...

[silene]

There are still some discrepancies. (Do not look too hard at the line numbers in the diff, I have manually edited it to only show the changes that are actually relevant to the package repository.) First, there are various changes in the title, synopsis, maintainers, comments, etc of the packages. So, nothing critical, but it would be good to include them to reduce the diff. Second, there are some important changes to the depends sections of rocq-core.opam and coqide-server.opam. Third, the conflicts parts of coq-core has been dropped, but I am unsure whether it is correct or not. Finally, I have no idea if the diff in the build section of coqide-server.opam is relevant or not.

--- ../coq/rocq-core.opam	2025-01-16 10:53:11.172958131 +0100
+++ core-dev/packages/rocq-core/rocq-core.9.0.dev/opam	2025-01-16 10:50:15.470410279 +0100
@@ -1,9 +1,7 @@
 synopsis: "The Rocq Prover with its prelude"
 description: """
-The Rocq Prover is an interactive theorem prover, or proof assistant. It provides
+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.
@@ -25,13 +23,13 @@
 bug-reports: "https://github.com/coq/coq/issues"
 depends: [
   "dune" {>= "3.8"}
-  "rocq-runtime" {= version}
+  "coq-core" {= version}
   "odoc" {with-doc}
 ]
 dev-repo: "git+https://github.com/coq/coq.git"
 build: [
   ["dune" "subst"] {dev}
-  # We tell dunestrap to use coq-config from rocq-runtime
+  # We tell dunestrap to use coq-config from coq-core
   [ make "dunestrap" "COQ_SPLIT=1" "DUNESTRAPOPT=-p rocq-core"]
   [
     "dune"

--- ../coq/rocq-runtime.opam	2025-01-16 10:53:11.172958131 +0100
+++ core-dev/packages/rocq-runtime/rocq-runtime.9.0.dev/opam	2025-01-16 10:50:15.470410279 +0100
@@ -1,9 +1,7 @@
 synopsis: "The Rocq Prover -- Core Binaries and Tools"
 description: """
-The Rocq Prover is an interactive theorem prover, or proof assistant. It provides
+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.
@@ -14,7 +12,7 @@
 formalization of mathematics (e.g. the full formalization of the
 Feit-Thompson theorem or homotopy type theory) and teaching.
 
-This package includes the Rocq Prover core binaries, plugins, and tools, but
+This package includes the Rocq core binaries, plugins, and tools, but
 not the vernacular standard library.
 
 Note that in this setup, Rocq needs to be started with the -boot and

--- ../coq/coqide-server.opam	2025-01-16 10:53:11.146958445 +0100
+++ core-dev/packages/coqide-server/coqide-server.9.0.dev/opam	2025-01-16 10:50:15.470410279 +0100
@@ -1,26 +1,24 @@
-synopsis: "The Rocq Prover, XML protocol server"
+synopsis: "The Coq Proof Assistant, XML protocol server"
 description: """
-The Rocq Prover is an interactive theorem prover, or proof assistant. It provides
+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.
 
 This package provides the `coqidetop` language server, an
-implementation of Rocq's [XML protocol](https://github.com/coq/coq/blob/master/dev/doc/xml-protocol.md)
-which allows clients, such as RocqIDE, to interact with the Rocq Prover in a
+implementation of Coq's [XML protocol](https://github.com/coq/coq/blob/master/dev/doc/xml-protocol.md)
+which allows clients, such as CoqIDE, to interact with Coq in a
 structured way."""
-maintainer: ["The Rocq development team <coqdev@inria.fr>"]
-authors: ["The Rocq development team, INRIA, CNRS, and contributors"]
+maintainer: ["The Coq development team <coqdev@inria.fr>"]
+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"}
-  "rocq-runtime" {= version}
+  "dune" {>= "2.9"}
+  "coq-core" {= version}
   "odoc" {with-doc}
 ]
 build: [
@@ -32,9 +30,15 @@
     name
     "-j"
     jobs
+    "--promote-install-files=false"
     "@install"
     "@runtest" {with-test}
     "@doc" {with-doc}
   ]
+  ["dune" "install" "-p" name "--create-install-files" name]
 ]
 dev-repo: "git+https://github.com/coq/coq.git"

--- ../coq/coq-core.opam	2025-01-16 10:53:11.146958445 +0100
+++ core-dev/packages/coq-core/coq-core.9.0.dev/opam	2025-01-16 10:50:15.469410295 +0100
@@ -1,9 +1,7 @@
 synopsis: "Compatibility binaries for Coq after the Rocq renaming"
-maintainer: ["The Rocq development team <coqdev@inria.fr>"]
-authors: ["The Rocq development team, INRIA, CNRS, and contributors"]
+maintainer: ["The Coq development team <coqdev@inria.fr>"]
+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/"
@@ -13,6 +11,11 @@
   "rocq-runtime" {= version}
   "odoc" {with-doc}
 ]
+conflicts: [
+  "coq"   { < "8.17" }
+]
+depopts: ["coq-native"]
+dev-repo: "git+https://github.com/coq/coq.git"
 build: [
   ["dune" "subst"] {dev}
   [
@@ -27,4 +30,7 @@
     "@doc" {with-doc}
   ]
 ]
-dev-repo: "git+https://github.com/coq/coq.git"

[proux01]

Third, the conflicts parts of coq-core has been dropped, but I am unsure whether it is correct or not.

coq-core.9.0.dev is only a shim, so any conflict from older coq-core packages should now be on rocq-runtime (which is the Rocq equivalent of previous coq-core in some sense)

[silene]

any conflict from older coq-core packages should now be on rocq-runtime

That was my sentiment as well, but since there is no conflicts in rocq-runtime, it means we are missing it.

Actually, rocq-runtime should also be made to conflict with any coq-core package, should it not?

[proux01]

any conflict from older coq-core packages should now be on rocq-runtime

That was my sentiment as well, but since there is no conflicts in rocq-runtime, it means we are missing it.

Indeed

Actually, rocq-runtime should also be made to conflict with any coq-core package, should it not?

Not for the same version because coq-core -> rocq-runtime so that would make it uninstallable.
But having rocq-runtime and coq-core < 9 indeed seem like a terrible combination we should probably forbid, good point.