Merge pull request #3289 from ppedrot/branch-9.0

Add the opam files for the 9.0 branch.

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

@@ -0,0 +1,36 @@
+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"]
+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}
+  "odoc" {with-doc}
+]
+conflicts: [
+  "coq"   { < "8.17" }
+]
+depopts: ["coq-native"]
+dev-repo: "git+https://github.com/coq/coq.git"
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
+
+url {
+  src: "git+https://github.com/coq/coq.git#master"
+}

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

@@ -0,0 +1,44 @@
+opam-version: "2.0"
+synopsis: "The Coq Proof Assistant, XML protocol server"
+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.
+
+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
+structured way."""
+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"}
+  "coq-core" {= version}
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "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]
+]
+dev-repo: "git+https://github.com/coq/coq.git"
+
+url {
+  src: "git+https://github.com/coq/coq.git#master"
+}

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

@@ -0,0 +1,52 @@
+opam-version: "2.0"
+synopsis: "The Rocq Prover with its prelude"
+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 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 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"}
+  "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"
+}

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

@@ -0,0 +1,65 @@
+opam-version: "2.0"
+synopsis: "The Rocq Prover -- Core Binaries and Tools"
+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 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
+-noinit options, as will otherwise fail to find the regular Rocq
+prelude, now living in the rocq-core package."""
+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" & < "3.14"}
+  "ocaml" {>= "4.09.0"}
+  "ocamlfind" {>= "1.8.1"}
+  "zarith" {>= "1.11"}
+  "conf-linux-libc-dev" {os = "linux"}
+  "odoc" {with-doc}
+]
+conflicts: [
+  "coq"   { < "8.17" }
+]
+depopts: ["coq-native"]
+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}
+  ]
+  [
+    "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"
+}