this repo has no description
anil.recoil.org
1opam-version: "2.0"
2synopsis: "The Coq Proof Assistant -- Standard Library"
3description: """
4Coq is a formal proof management system. It provides
5a formal language to write mathematical definitions, executable
6algorithms and theorems together with an environment for
7semi-interactive development of machine-checked proofs.
8
9Typical applications include the certification of properties of
10programming languages (e.g. the CompCert compiler certification
11project, or the Bedrock verified low-level programming library), the
12formalization of mathematics (e.g. the full formalization of the
13Feit-Thompson theorem or homotopy type theory) and teaching.
14
15This package includes the Coq Standard Library, that is to say, the
16set of modules usually bound to the Coq.* namespace."""
17maintainer: ["The Coq development team <coqdev@inria.fr>"]
18authors: ["The Coq development team, INRIA, CNRS, and contributors"]
19license: "LGPL-2.1-only"
20homepage: "https://coq.inria.fr/"
21doc: "https://coq.github.io/doc/"
22bug-reports: "https://github.com/coq/coq/issues"
23depends: [
24 "dune" {>= "2.9"}
25 "coq-core" {= version}
26]
27build: [
28 [ "./configure"
29 "-prefix" prefix
30 "-mandir" man
31 "-libdir" "%{lib}%/coq"
32 "-native-compiler" "yes" {coq-native:installed} "no" {!coq-native:installed}
33 ]
34 [ make "dunestrap" "COQ_DUNE_EXTRA_OPT=-split" ]
35 [
36 "dune"
37 "build"
38 "-p"
39 name
40 "-j"
41 jobs
42 "@install"
43 "@runtest" {with-test}
44 "@doc" {with-doc}
45 ]
46]
47dev-repo: "git+https://github.com/coq/coq.git"
48depopts: ["coq-native"]
49
50url {
51 src: "https://github.com/coq/coq/releases/download/V8.17.1/coq-8.17.1.tar.gz"
52 checksum: "sha512=9a35311acec2a806730b94ac7dceabc88837f235c52a14c026827d9b89433bd7fa9555a9fc6829aa49edfedb24c8bbaf1411ebf463b74a50aeb17cba47745b6b"
53}