[core-dev] 9.0 Update according to tag V9.0+rc1 in coq/coq repo

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

@@ -0,0 +1,34 @@
+opam-version: "2.0"
+synopsis: "Compatibility metapackage for Coq Stdlib library after the Rocq renaming"
+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/stdlib/issues"
+depends: [
+  "dune" {>= "3.8"}
+  "coq-core"
+  "rocq-stdlib" {= version}
+  "odoc" {with-doc}
+]
+dev-repo: "git+https://github.com/coq/stdlib.git"
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dev/with-rocq-wrap.sh"
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
+
+url {
+  src: "git+https://github.com/coq/stdlib.git#V9.0+rc1"
+}

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

@@ -0,0 +1,44 @@
+opam-version: "2.0"
+synopsis: "Compatibility metapackage for Coq after the Rocq renaming"
+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" {>= "3.8"}
+  "rocq-prover" {= version}
+  "coq-core" {= version}
+  "coq-stdlib"
+  "coqide-server" {= version}
+  "odoc" {with-doc}
+]
+dev-repo: "git+https://github.com/coq/coq.git"
+build: [
+  ["dune" "subst"] {dev}
+  [ "./configure"
+    "-release" # -release must be the first command line argument
+    "-prefix" prefix
+    "-mandir" man
+    "-libdir" "%{lib}%/coq"
+    "-native-compiler" "yes" {rocq-native:installed} "no" {!rocq-native:installed}
+  ] {with-test}
+  [
+    "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#v9.0"
+}

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

@@ -0,0 +1,49 @@
+opam-version: "2.0"
+synopsis: "The Rocq Prover with Stdlib"
+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 is a virtual package gathering the rocq-core and rocq-stdlib packages."""
+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" {>= "3.8"}
+  "rocq-core" {= version}
+  "rocq-stdlib"
+  "ounit2" {with-test}
+  "conf-python-3" {with-test}
+  "conf-time" {with-test}
+  "odoc" {with-doc}
+]
+dev-repo: "git+https://github.com/coq/coq.git"
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    "rocq"
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
+
+url {
+  src: "git+https://github.com/coq/coq.git#v9.0"
+}

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

@@ -32,15 +32,16 @@ depends: [
   "conf-linux-libc-dev" {os = "linux"}
   "odoc" {with-doc}
 ]
+depopts: ["rocq-native" "memprof-limits" "memtrace"]
 conflicts: [
   "coq" { < "8.17" }
   "coq-core" { < "8.21" }
 ]
-depopts: ["rocq-native" "memprof-limits" "memtrace"]
 dev-repo: "git+https://github.com/coq/coq.git"
 build: [
   ["dune" "subst"] {dev}
   [ "./configure"
+    "-release" # -release must be the first command line argument
     "-prefix" prefix
     "-mandir" man
     "-libdir" "%{lib}%/coq"

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

@@ -0,0 +1,49 @@
+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/stdlib/issues"
+depends: [
+  "dune" {>= "3.8"}
+  "rocq-runtime"
+  "rocq-core" {= version}
+  "odoc" {with-doc}
+]
+depopts: ["coq-native"]
+dev-repo: "git+https://github.com/coq/stdlib.git"
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dev/with-rocq-wrap.sh"
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
+
+url {
+  src: "git+https://github.com/coq/stdlib.git#V9.0+rc1"
+}

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

@@ -0,0 +1,45 @@
+opam-version: "2.0"
+synopsis: "The Rocq Prover --- GTK3 IDE"
+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.
+
+This package provides the RocqIDE, a graphical user interface for the
+development of interactive proofs."""
+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" {>= "3.8"}
+  "ocamlfind" {build}
+  "conf-findutils" {build}
+  "conf-adwaita-icon-theme"
+  "coqide-server" {= version}
+  "cairo2" {>= "0.6.4"}
+  "lablgtk3-sourceview3" {>= "3.1.2" & (>= "3.1.5" | os != "windows")}
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
+dev-repo: "git+https://github.com/coq/coq.git"
+
+url {
+  src: "git+https://github.com/coq/coq.git#v9.0"
+}