more 9.0.dev fixes

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

@@ -1,7 +1,21 @@
 opam-version: "2.0"
 synopsis: "Compatibility binaries for Coq after the Rocq renaming"
-maintainer: ["The Coq development team <[email protected]>"]
-authors: ["The Coq development team, INRIA, CNRS, and contributors"]
+description: """
+The Rocq Prover is an interactive theorem prover, or proof assistant. 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 compatibility binaries to call Rocq
+through previous Coq commands like coqc coqtop,..."""
+maintainer: ["The Rocq development team <[email protected]>"]
+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/"
@@ -11,10 +25,6 @@ depends: [
   "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}

core-dev/packages/coqide-server/coqide-server.9.0.dev/opam

@@ -1,24 +1,24 @@
 opam-version: "2.0"
-synopsis: "The Coq Proof Assistant, XML protocol server"
+synopsis: "The Rocq Prover, XML protocol server"
 description: """
-Coq is a formal proof management system. It provides
+The Rocq Prover is an interactive theorem prover, or proof assistant. 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 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
+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
 structured way."""
-maintainer: ["The Coq development team <[email protected]>"]
-authors: ["The Coq development team, INRIA, CNRS, and contributors"]
+maintainer: ["The Rocq development team <[email protected]>"]
+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" {>= "2.9"}
-  "coq-core" {= version}
+  "dune" {>= "3.8"}
+  "rocq-runtime" {= version}
   "odoc" {with-doc}
 ]
 build: [
@@ -30,12 +30,10 @@ build: [
     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"
 

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

@@ -1,7 +1,7 @@
 opam-version: "2.0"
 synopsis: "The Rocq Prover with its prelude"
 description: """
-Rocq is a formal proof management system. It provides
+The Rocq Prover is an interactive theorem prover, or proof assistant. 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.
@@ -23,14 +23,13 @@ doc: "https://coq.github.io/doc/"
 bug-reports: "https://github.com/coq/coq/issues"
 depends: [
   "dune" {>= "3.8"}
-  "coq-core" {= version}
+  "rocq-runtime" {= 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
+  # We tell dunestrap to use coq-config from rocq-runtime
   [ make "dunestrap" "COQ_SPLIT=1" "DUNESTRAPOPT=-p rocq-core"]
   [
     "dune"

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

@@ -1,7 +1,7 @@
 opam-version: "2.0"
 synopsis: "The Rocq Prover -- Core Binaries and Tools"
 description: """
-Rocq is a formal proof management system. It provides
+The Rocq Prover is an interactive theorem prover, or proof assistant. 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.
@@ -12,7 +12,7 @@ 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 core binaries, plugins, and tools, but
+This package includes the Rocq Prover 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
@@ -33,17 +33,17 @@ depends: [
   "odoc" {with-doc}
 ]
 conflicts: [
-  "coq"   { < "8.17" }
+  "coq"   { < "8.21" }
 ]
-depopts: ["coq-native"]
+depopts: ["rocq-native" "memprof-limits" "memtrace"]
 dev-repo: "git+https://github.com/coq/coq.git"
 build: [
   ["dune" "subst"] {dev}
   [ "./configure"
     "-prefix" prefix
     "-mandir" man
     "-libdir" "%{lib}%/coq"
-    "-native-compiler" "yes" {coq-native:installed} "no" {!coq-native:installed}
+    "-native-compiler" "yes" {rocq-native:installed} "no" {!rocq-native:installed}
   ]
   [
     "dune"