From fede298ddbdf0fb57e1aa45f2441ab7333476a6c Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 7 Nov 2021 23:17:38 +0100 Subject: [PATCH] [coq.dev] New upstream split package setup. This should work fine once coq/coq#15560 is merged. From today, the canonical opam packages live in Coq's repository. --- core-dev/packages/coq-core/coq-core.dev/opam | 55 +++++++++++++ .../packages/coq-stdlib/coq-stdlib.dev/opam | 55 +++++++++++++ core-dev/packages/coq/coq.dev/opam | 77 ++++++++----------- 3 files changed, 142 insertions(+), 45 deletions(-) create mode 100644 core-dev/packages/coq-core/coq-core.dev/opam create mode 100644 core-dev/packages/coq-stdlib/coq-stdlib.dev/opam diff --git a/core-dev/packages/coq-core/coq-core.dev/opam b/core-dev/packages/coq-core/coq-core.dev/opam new file mode 100644 index 0000000000..95f8a5f2df --- /dev/null +++ b/core-dev/packages/coq-core/coq-core.dev/opam @@ -0,0 +1,55 @@ +# This file is generated by dune, edit dune-project instead +opam-version: "2.0" +version: "dev" +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} +] +build: [ + # Requires dune 2.8 due to https://github.com/ocaml/dune/issues/3219 + # ["dune" "subst"] {pinned} + # + # XXX need to run configure as in coq-core, or else dunestrap will + # use the default rule in config + [ "./configure" + "-prefix" prefix + "-mandir" man + "-libdir" "%{lib}%/coq" + "-coqide" "no" + "-native-compiler" "yes" {coq-native:installed} "no" {!coq-native:installed} + ] + [ make "dunestrap" "COQ_DUNE_EXTRA_OPT=-split" ] + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] +] +dev-repo: "git+https://github.com/coq/coq.git" diff --git a/core-dev/packages/coq-stdlib/coq-stdlib.dev/opam b/core-dev/packages/coq-stdlib/coq-stdlib.dev/opam new file mode 100644 index 0000000000..95f8a5f2df --- /dev/null +++ b/core-dev/packages/coq-stdlib/coq-stdlib.dev/opam @@ -0,0 +1,55 @@ +# This file is generated by dune, edit dune-project instead +opam-version: "2.0" +version: "dev" +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} +] +build: [ + # Requires dune 2.8 due to https://github.com/ocaml/dune/issues/3219 + # ["dune" "subst"] {pinned} + # + # XXX need to run configure as in coq-core, or else dunestrap will + # use the default rule in config + [ "./configure" + "-prefix" prefix + "-mandir" man + "-libdir" "%{lib}%/coq" + "-coqide" "no" + "-native-compiler" "yes" {coq-native:installed} "no" {!coq-native:installed} + ] + [ make "dunestrap" "COQ_DUNE_EXTRA_OPT=-split" ] + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] +] +dev-repo: "git+https://github.com/coq/coq.git" diff --git a/core-dev/packages/coq/coq.dev/opam b/core-dev/packages/coq/coq.dev/opam index e4c5bd8fd6..3a2aa1fb18 100644 --- a/core-dev/packages/coq/coq.dev/opam +++ b/core-dev/packages/coq/coq.dev/opam @@ -1,54 +1,41 @@ +# This file is generated by dune, edit dune-project instead opam-version: "2.0" -maintainer: "coqdev@inria.fr" -authors: "The Coq development team, INRIA, CNRS, and contributors." -homepage: "https://coq.inria.fr/" -bug-reports: "https://github.com/coq/coq/issues" -dev-repo: "git+https://github.com/coq/coq.git" -license: "LGPL-2.1-only" -synopsis: "Formal proof management system" +version: "dev" +synopsis: "The Coq Proof Assistant" description: """ -The Coq proof assistant 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 and the -Bedrock verified low-level programming library), the formalization of -mathematics (e.g., the full formalization of the Feit-Thompson theorem -and homotopy type theory) and teaching. -""" +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. -depopts: [ - "coq-native" -] +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: [ - "ocaml" {>= "4.09.0"} - "ocamlfind" {build} - "dune" {>= "2.5.1"} - "conf-findutils" {build} - "zarith" {>= "1.10"} -] -conflicts: [ - "base-nnp" - "ocaml-option-nnpchecker" + "dune" {>= "2.9"} + "coq-core" {= version} + "coq-stdlib" {= version} ] build: [ + ["dune" "subst"] {pinned} [ - "./configure" - "-configdir" "%{lib}%/coq/config" - "-prefix" prefix - "-mandir" man - "-docdir" "%{doc}%/coq" - "-libdir" "%{lib}%/coq" - "-datadir" "%{share}%/coq" - "-coqide" "no" - "-native-compiler" "yes" {coq-native:installed} "no" {!coq-native:installed} + "dune" + "build" + "-p" + name + "-j" + jobs + "@install" + "@runtest" {with-test} + "@doc" {with-doc} ] - [ make "COQ_USE_DUNE=" "-j%{jobs}%" ] ] -install: [ - [ make "COQ_USE_DUNE=" "install" ] -] - -url { - src: "git+https://github.com/coq/coq.git#master" -} +dev-repo: "git+https://github.com/coq/coq.git"