From 1a5cb829726a07f1da5f00959f76d34d2b7aec90 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 24 Jan 2025 17:50:04 +0100 Subject: [PATCH] [core-dev] Add Rocq 9.0+rc1 --- .../packages/coq-core/coq-core.9.0+rc1/opam | 51 +++++++++++++ core-dev/packages/coq/coq.9.0+rc1/opam | 50 +++++++++++++ .../coqide-server/coqide-server.9.0+rc1/opam | 47 ++++++++++++ .../packages/rocq-core/rocq-core.9.0+rc1/opam | 56 +++++++++++++++ .../rocq-prover/rocq-prover.9.0+rc1/opam | 54 ++++++++++++++ .../rocq-runtime/rocq-runtime.9.0+rc1/opam | 72 +++++++++++++++++++ .../packages/rocqide/rocqide.9.0+rc1/opam | 50 +++++++++++++ 7 files changed, 380 insertions(+) create mode 100644 core-dev/packages/coq-core/coq-core.9.0+rc1/opam create mode 100644 core-dev/packages/coq/coq.9.0+rc1/opam create mode 100644 core-dev/packages/coqide-server/coqide-server.9.0+rc1/opam create mode 100644 core-dev/packages/rocq-core/rocq-core.9.0+rc1/opam create mode 100644 core-dev/packages/rocq-prover/rocq-prover.9.0+rc1/opam create mode 100644 core-dev/packages/rocq-runtime/rocq-runtime.9.0+rc1/opam create mode 100644 core-dev/packages/rocqide/rocqide.9.0+rc1/opam diff --git a/core-dev/packages/coq-core/coq-core.9.0+rc1/opam b/core-dev/packages/coq-core/coq-core.9.0+rc1/opam new file mode 100644 index 000000000..dcc4b51b9 --- /dev/null +++ b/core-dev/packages/coq-core/coq-core.9.0+rc1/opam @@ -0,0 +1,51 @@ +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 "] +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-runtime" {= version} + "odoc" {with-doc} +] +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: + "https://github.com/coq/coq/releases/download/V9.0+rc1/coq-9.0-rc1.tar.gz" + checksum: [ + "md5=ebb23830fc6d43a1d955d28bdccfd7d5" + "sha512=31cb5eca83620ac5f517422f445c37a9345f3ba973f43db9101996d45368856e07e2c4b4ebb2103c169f742aeef095026b2c947765b78be51bfe7fdf43b5d693" + ] +} diff --git a/core-dev/packages/coq/coq.9.0+rc1/opam b/core-dev/packages/coq/coq.9.0+rc1/opam new file mode 100644 index 000000000..03d46dd7e --- /dev/null +++ b/core-dev/packages/coq/coq.9.0+rc1/opam @@ -0,0 +1,50 @@ +opam-version: "2.0" +synopsis: "Compatibility metapackage for Coq after the Rocq renaming" +maintainer: ["The Rocq 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/coq/issues" +depends: [ + "dune" {>= "3.8"} + "rocq-prover" {= version} + "coq-core" {= version} + "coq-stdlib" + "coqide-server" {= version} + "ounit2" {with-test} + "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: + "https://github.com/coq/coq/releases/download/V9.0+rc1/coq-9.0-rc1.tar.gz" + checksum: [ + "md5=ebb23830fc6d43a1d955d28bdccfd7d5" + "sha512=31cb5eca83620ac5f517422f445c37a9345f3ba973f43db9101996d45368856e07e2c4b4ebb2103c169f742aeef095026b2c947765b78be51bfe7fdf43b5d693" + ] +} diff --git a/core-dev/packages/coqide-server/coqide-server.9.0+rc1/opam b/core-dev/packages/coqide-server/coqide-server.9.0+rc1/opam new file mode 100644 index 000000000..ba82a3235 --- /dev/null +++ b/core-dev/packages/coqide-server/coqide-server.9.0+rc1/opam @@ -0,0 +1,47 @@ +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/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 Rocq 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/coq/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/coq/coq.git" + +url { + src: + "https://github.com/coq/coq/releases/download/V9.0+rc1/coq-9.0-rc1.tar.gz" + checksum: [ + "md5=ebb23830fc6d43a1d955d28bdccfd7d5" + "sha512=31cb5eca83620ac5f517422f445c37a9345f3ba973f43db9101996d45368856e07e2c4b4ebb2103c169f742aeef095026b2c947765b78be51bfe7fdf43b5d693" + ] +} diff --git a/core-dev/packages/rocq-core/rocq-core.9.0+rc1/opam b/core-dev/packages/rocq-core/rocq-core.9.0+rc1/opam new file mode 100644 index 000000000..a706f23c4 --- /dev/null +++ b/core-dev/packages/rocq-core/rocq-core.9.0+rc1/opam @@ -0,0 +1,56 @@ +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 "] +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-runtime" {= 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 + [ 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/coq/coq/releases/download/V9.0+rc1/coq-9.0-rc1.tar.gz" + checksum: [ + "md5=ebb23830fc6d43a1d955d28bdccfd7d5" + "sha512=31cb5eca83620ac5f517422f445c37a9345f3ba973f43db9101996d45368856e07e2c4b4ebb2103c169f742aeef095026b2c947765b78be51bfe7fdf43b5d693" + ] +} diff --git a/core-dev/packages/rocq-prover/rocq-prover.9.0+rc1/opam b/core-dev/packages/rocq-prover/rocq-prover.9.0+rc1/opam new file mode 100644 index 000000000..7ec6c997a --- /dev/null +++ b/core-dev/packages/rocq-prover/rocq-prover.9.0+rc1/opam @@ -0,0 +1,54 @@ +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 "] +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: + "https://github.com/coq/coq/releases/download/V9.0+rc1/coq-9.0-rc1.tar.gz" + checksum: [ + "md5=ebb23830fc6d43a1d955d28bdccfd7d5" + "sha512=31cb5eca83620ac5f517422f445c37a9345f3ba973f43db9101996d45368856e07e2c4b4ebb2103c169f742aeef095026b2c947765b78be51bfe7fdf43b5d693" + ] +} diff --git a/core-dev/packages/rocq-runtime/rocq-runtime.9.0+rc1/opam b/core-dev/packages/rocq-runtime/rocq-runtime.9.0+rc1/opam new file mode 100644 index 000000000..bc63a9975 --- /dev/null +++ b/core-dev/packages/rocq-runtime/rocq-runtime.9.0+rc1/opam @@ -0,0 +1,72 @@ +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 "] +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} +] +depopts: ["rocq-native" "memprof-limits" "memtrace"] +conflicts: [ + "coq" { < "8.17" } + "coq-core" { < "8.21" } +] +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} + ] + [ + "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/coq/coq/releases/download/V9.0+rc1/coq-9.0-rc1.tar.gz" + checksum: [ + "md5=ebb23830fc6d43a1d955d28bdccfd7d5" + "sha512=31cb5eca83620ac5f517422f445c37a9345f3ba973f43db9101996d45368856e07e2c4b4ebb2103c169f742aeef095026b2c947765b78be51bfe7fdf43b5d693" + ] +} diff --git a/core-dev/packages/rocqide/rocqide.9.0+rc1/opam b/core-dev/packages/rocqide/rocqide.9.0+rc1/opam new file mode 100644 index 000000000..2e190b0ce --- /dev/null +++ b/core-dev/packages/rocqide/rocqide.9.0+rc1/opam @@ -0,0 +1,50 @@ +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 "] +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: + "https://github.com/coq/coq/releases/download/V9.0+rc1/coq-9.0-rc1.tar.gz" + checksum: [ + "md5=ebb23830fc6d43a1d955d28bdccfd7d5" + "sha512=31cb5eca83620ac5f517422f445c37a9345f3ba973f43db9101996d45368856e07e2c4b4ebb2103c169f742aeef095026b2c947765b78be51bfe7fdf43b5d693" + ] +}