Add Rocq 9.1+rc1

packages/coq-core/coq-core.9.1+rc1/opam

@@ -0,0 +1,50 @@
+opam-version: "2.0"
+synopsis: "Compatibility binaries for Coq after the Rocq renaming"
+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://rocq-prover.org/"
+doc: "https://rocq-prover.org/docs/"
+bug-reports: "https://github.com/rocq-prover/rocq/issues"
+depends: [
+  "dune" {>= "3.8"}
+  "rocq-runtime" {= version}
+  "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/rocq-prover/rocq.git"
+post-messages: [
+  "Coq has been renamed to The Rocq Prover, see https://rocq-prover.org/refman/changes.html#porting-to-the-rocq-prover for details. 
+   This package provides compatibility binaries to ease the transition to the new rocq binary."
+]
+url {
+  src: "https://github.com/rocq-prover/rocq/releases/download/V9.1%2Brc1/rocq-9.1-rc1.tar.gz"
+  checksum: "sha512=3178091897ad24dab1cac9a3326da56b794eedfbfc900ba9cd652c4bd7f1b290da97961f887fb553562f3d0cbfa7e03ff83bafdf7c75c9e453171d5d6db79571"
+}

packages/coq-lsp/coq-lsp.0.2.3+9.0/opam

@@ -36,7 +36,8 @@ depends: [
   # unit testing
   "ppx_inline_test"     { >= "v0.15.0" }
 
-  "rocq-prover"         { >= "9.0" < "9.1" }
+  "rocq-core"    { >= "9.0" < "9.1" }
+  "rocq-stdlib"
 
   # [release branch] Remove
   "ocamlfind" {>= "1.9.1" & (>= "1.9.8" | os != "windows") }

packages/coq/coq.9.1+rc1/opam

@@ -0,0 +1,14 @@
+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://rocq-prover.org/"
+doc: "https://rocq-prover.org/docs/"
+bug-reports: "https://github.com/rocq-prover/rocq/issues"
+depends: [
+  "coq-core" {= version}
+  "coq-stdlib" {= "9.0.0"}
+  "coqide-server" {= version}
+]
+dev-repo: "git+https://github.com/rocq-prover/rocq.git"

packages/coqide-server/coqide-server.9.1+rc1/opam

@@ -0,0 +1,42 @@
+opam-version: "2.0"
+synopsis: "The Rocq Prover, XML protocol server"
+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 `coqidetop` language server, an
+implementation of Rocq's [XML protocol](https://github.com/rocq-prover/rocq/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 Rocq development team <[email protected]>"]
+authors: ["The Rocq development team, INRIA, CNRS, and contributors"]
+license: "LGPL-2.1-only"
+homepage: "https://rocq-prover.org/"
+doc: "https://rocq-prover.org/docs/"
+bug-reports: "https://github.com/rocq-prover/rocq/issues"
+depends: [
+  "dune" {>= "3.8"}
+  "rocq-runtime" {= version}
+  "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/rocq-prover/rocq.git"
+url {
+  src: "https://github.com/rocq-prover/rocq/releases/download/V9.1%2Brc1/rocq-9.1-rc1.tar.gz"
+  checksum: "sha512=3178091897ad24dab1cac9a3326da56b794eedfbfc900ba9cd652c4bd7f1b290da97961f887fb553562f3d0cbfa7e03ff83bafdf7c75c9e453171d5d6db79571"
+}

packages/rocq-core/rocq-core.9.1+rc1/opam

@@ -0,0 +1,51 @@
+opam-version: "2.0"
+synopsis: "The Rocq Prover with its prelude"
+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 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://rocq-prover.org/"
+doc: "https://rocq-prover.org/docs/"
+bug-reports: "https://github.com/rocq-prover/rocq/issues"
+depends: [
+  "dune" {>= "3.8"}
+  "rocq-runtime" {= version}
+  "odoc" {with-doc}
+]
+dev-repo: "git+https://github.com/rocq-prover/rocq.git"
+build: [
+  ["dune" "subst"] {dev}
+  # We tell dunestrap to use coq-config from rocq-runtime
+  [ 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: "https://github.com/rocq-prover/rocq/releases/download/V9.1%2Brc1/rocq-9.1-rc1.tar.gz"
+  checksum: "sha512=3178091897ad24dab1cac9a3326da56b794eedfbfc900ba9cd652c4bd7f1b290da97961f887fb553562f3d0cbfa7e03ff83bafdf7c75c9e453171d5d6db79571"
+}

packages/rocq-devtools/rocq-devtools.9.1+rc1/opam

@@ -0,0 +1,48 @@
+opam-version: "2.0"
+synopsis: "Development tools for Rocq"
+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 tools to help when developing Rocq projects
+(timelog2html)."""
+maintainer: ["The Rocq development team <[email protected]>"]
+authors: ["The Rocq development team, INRIA, CNRS, and contributors"]
+license: "LGPL-2.1-only"
+homepage: "https://rocq-prover.org/"
+doc: "https://rocq-prover.org/docs/"
+bug-reports: "https://github.com/rocq-prover/rocq/issues"
+depends: [
+  "dune" {>= "3.8"}
+  "rocq-runtime" {= version}
+  "yojson" {>= "2.0"}
+  "camlzip"
+  "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/rocq-prover/rocq.git"
+url {
+  src: "https://github.com/rocq-prover/rocq/releases/download/V9.1%2Brc1/rocq-9.1-rc1.tar.gz"
+  checksum: "sha512=3178091897ad24dab1cac9a3326da56b794eedfbfc900ba9cd652c4bd7f1b290da97961f887fb553562f3d0cbfa7e03ff83bafdf7c75c9e453171d5d6db79571"
+}

packages/rocq-runtime/rocq-runtime.9.1+rc1/opam

@@ -0,0 +1,67 @@
+opam-version: "2.0"
+synopsis: "The Rocq Prover -- Core Binaries and Tools"
+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 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
+-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://rocq-prover.org/"
+doc: "https://rocq-prover.org/docs/"
+bug-reports: "https://github.com/rocq-prover/rocq/issues"
+depends: [
+  "dune" {>= "3.8"}
+  "ocaml" {>= "4.14.0"}
+  "ocamlfind" {>= "1.9.1" & (>= "1.9.8" | os != "windows")}
+  "zarith" {>= "1.11"}
+  "conf-linux-libc-dev" {os = "linux"}
+  "odoc" {with-doc}
+]
+depopts: ["rocq-native" "memprof-limits" "memtrace"]
+conflicts: [
+  "coq" {< "8.17"}
+  "coq-core" {< "8.21"}
+]
+dev-repo: "git+https://github.com/rocq-prover/rocq.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}
+  ]
+  [
+    "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: "https://github.com/rocq-prover/rocq/releases/download/V9.1%2Brc1/rocq-9.1-rc1.tar.gz"
+  checksum: "sha512=3178091897ad24dab1cac9a3326da56b794eedfbfc900ba9cd652c4bd7f1b290da97961f887fb553562f3d0cbfa7e03ff83bafdf7c75c9e453171d5d6db79571"
+}

packages/rocqide/rocqide.9.1+rc1/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://rocq-prover.org/"
+doc: "https://rocq-prover.org/docs/"
+bug-reports: "https://github.com/rocq-prover/rocq/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/rocq-prover/rocq.git"
+url {
+  src: "https://github.com/rocq-prover/rocq/releases/download/V9.1%2Brc1/rocq-9.1-rc1.tar.gz"
+  checksum: "sha512=3178091897ad24dab1cac9a3326da56b794eedfbfc900ba9cd652c4bd7f1b290da97961f887fb553562f3d0cbfa7e03ff83bafdf7c75c9e453171d5d6db79571"
+}