-
Notifications
You must be signed in to change notification settings - Fork 166
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
[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.
- Loading branch information
Showing
3 changed files
with
142 additions
and
45 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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 <[email protected]>"] | ||
| 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" |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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 <[email protected]>"] | ||
| 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" |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,54 +1,41 @@ | ||
| # This file is generated by dune, edit dune-project instead | ||
| opam-version: "2.0" | ||
| maintainer: "[email protected]" | ||
| 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 <[email protected]>"] | ||
| 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" |