diff --git a/core-dev/packages/coq-stdlib/coq-stdlib.9.0+rc1/opam b/core-dev/packages/coq-stdlib/coq-stdlib.9.0+rc1/opam new file mode 100644 index 000000000..2c8c7c8df --- /dev/null +++ b/core-dev/packages/coq-stdlib/coq-stdlib.9.0+rc1/opam @@ -0,0 +1,38 @@ +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: + "https://github.com/coq/stdlib/releases/download/V9.0+rc1/stdlib-9.0-rc1.tar.gz" + checksum: [ + "sha512=413f457db022ddb635c18bf04fed48025c23ac1d69dfadc12e889d86dca44d8e1e4fe1e53caac03b881c9b79cf74063e540e369a800c167e386a9ae53a025b9e" + ] +} diff --git a/core-dev/packages/coq/coq.9.0.dev/opam b/core-dev/packages/coq/coq.9.0.dev/opam new file mode 100644 index 000000000..dd569e65b --- /dev/null +++ b/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 "] +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" +} diff --git a/core-dev/packages/rocq-prover/rocq-prover.9.0.dev/opam b/core-dev/packages/rocq-prover/rocq-prover.9.0.dev/opam new file mode 100644 index 000000000..f82a9f735 --- /dev/null +++ b/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 "] +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" +} diff --git a/core-dev/packages/rocq-runtime/rocq-runtime.9.0.dev/opam b/core-dev/packages/rocq-runtime/rocq-runtime.9.0.dev/opam index 1b5af7ff9..f822f5b25 100644 --- a/core-dev/packages/rocq-runtime/rocq-runtime.9.0.dev/opam +++ b/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" diff --git a/core-dev/packages/rocq-stdlib/rocq-stdlib.9.0+rc1/opam b/core-dev/packages/rocq-stdlib/rocq-stdlib.9.0+rc1/opam new file mode 100644 index 000000000..837193271 --- /dev/null +++ b/core-dev/packages/rocq-stdlib/rocq-stdlib.9.0+rc1/opam @@ -0,0 +1,53 @@ +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" {>= "9.0" & < "9.1~"} + "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: + "https://github.com/coq/stdlib/releases/download/V9.0+rc1/stdlib-9.0-rc1.tar.gz" + checksum: [ + "sha512=413f457db022ddb635c18bf04fed48025c23ac1d69dfadc12e889d86dca44d8e1e4fe1e53caac03b881c9b79cf74063e540e369a800c167e386a9ae53a025b9e" + ] +} diff --git a/core-dev/packages/rocqide/rocqide.9.0.dev/opam b/core-dev/packages/rocqide/rocqide.9.0.dev/opam new file mode 100644 index 000000000..7a64fcd59 --- /dev/null +++ b/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 "] +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" +}