From bb067fadecb0141c40fbb610d1b86eb86bd2bc8a Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Fri, 26 Jan 2024 08:18:22 +0100 Subject: [PATCH] add coq-core.8.19.0, coq-stdlib.8.19.0, coqide-server.8.19.0, coq.8.19.0 --- packages/coq-core/coq-core.8.19.0/opam | 69 +++++++++++++++++++ packages/coq-stdlib/coq-stdlib.8.19.0/opam | 55 +++++++++++++++ packages/coq/coq.8.19.0/opam | 50 ++++++++++++++ .../coqide-server/coqide-server.8.19.0/opam | 48 +++++++++++++ 4 files changed, 222 insertions(+) create mode 100644 packages/coq-core/coq-core.8.19.0/opam create mode 100644 packages/coq-stdlib/coq-stdlib.8.19.0/opam create mode 100644 packages/coq/coq.8.19.0/opam create mode 100644 packages/coqide-server/coqide-server.8.19.0/opam diff --git a/packages/coq-core/coq-core.8.19.0/opam b/packages/coq-core/coq-core.8.19.0/opam new file mode 100644 index 00000000000..72236fe3277 --- /dev/null +++ b/packages/coq-core/coq-core.8.19.0/opam @@ -0,0 +1,69 @@ +opam-version: "2.0" +synopsis: "The Coq Proof Assistant -- Core Binaries and Tools" +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. + +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 Coq core binaries, plugins, and tools, but +not the vernacular standard library. + +Note that in this setup, Coq needs to be started with the -boot and +-noinit options, as will otherwise fail to find the regular Coq +prelude, now living in the coq-stdlib package.""" +maintainer: ["The Coq development team "] +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"} + "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: "https://github.com/coq/coq/releases/download/V8.19.0/coq-8.19.0.tar.gz" + checksum: [ + "md5=64b49dbc3205477bd7517642c0b9cbb6" + "sha512=02fb5b4fb575af79e092492cbec6dc0d15a1d74a07f827f657a72d4e6066532630e5a6d15be4acdb73314bd40b9a321f9ea0584e0ccfe51fd3a56353bd30db9b" + ] +} diff --git a/packages/coq-stdlib/coq-stdlib.8.19.0/opam b/packages/coq-stdlib/coq-stdlib.8.19.0/opam new file mode 100644 index 00000000000..45432c826eb --- /dev/null +++ b/packages/coq-stdlib/coq-stdlib.8.19.0/opam @@ -0,0 +1,55 @@ +opam-version: "2.0" +synopsis: "The Coq Proof Assistant -- Standard Library" +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. + +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 Coq Standard Library, that is to say, the +set of modules usually bound to the Coq.* namespace.""" +maintainer: ["The Coq development team "] +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} +] +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_DUNE_EXTRA_OPT=-split" "DUNESTRAPOPT=-p coq-stdlib"] + [ + "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/V8.19.0/coq-8.19.0.tar.gz" + checksum: [ + "md5=64b49dbc3205477bd7517642c0b9cbb6" + "sha512=02fb5b4fb575af79e092492cbec6dc0d15a1d74a07f827f657a72d4e6066532630e5a6d15be4acdb73314bd40b9a321f9ea0584e0ccfe51fd3a56353bd30db9b" + ] +} diff --git a/packages/coq/coq.8.19.0/opam b/packages/coq/coq.8.19.0/opam new file mode 100644 index 00000000000..9e12ad86aa1 --- /dev/null +++ b/packages/coq/coq.8.19.0/opam @@ -0,0 +1,50 @@ +opam-version: "2.0" +synopsis: "The Coq Proof Assistant" +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. + +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.""" +maintainer: ["The Coq development team "] +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} + "coq-stdlib" {= version} + "coqide-server" {= version} + "odoc" {with-doc} +] +dev-repo: "git+https://github.com/coq/coq.git" +build: [ + ["dune" "subst"] {dev} + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "--promote-install-files=false" + "@install" + "@doc" {with-doc} + ] + ["dune" "install" "-p" name "--create-install-files" name] +] + +url { + src: "https://github.com/coq/coq/releases/download/V8.19.0/coq-8.19.0.tar.gz" + checksum: [ + "md5=64b49dbc3205477bd7517642c0b9cbb6" + "sha512=02fb5b4fb575af79e092492cbec6dc0d15a1d74a07f827f657a72d4e6066532630e5a6d15be4acdb73314bd40b9a321f9ea0584e0ccfe51fd3a56353bd30db9b" + ] +} diff --git a/packages/coqide-server/coqide-server.8.19.0/opam b/packages/coqide-server/coqide-server.8.19.0/opam new file mode 100644 index 00000000000..db0b8100101 --- /dev/null +++ b/packages/coqide-server/coqide-server.8.19.0/opam @@ -0,0 +1,48 @@ +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 "] +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: "https://github.com/coq/coq/releases/download/V8.19.0/coq-8.19.0.tar.gz" + checksum: [ + "md5=64b49dbc3205477bd7517642c0b9cbb6" + "sha512=02fb5b4fb575af79e092492cbec6dc0d15a1d74a07f827f657a72d4e6066532630e5a6d15be4acdb73314bd40b9a321f9ea0584e0ccfe51fd3a56353bd30db9b" + ] +}