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" {>= "3.6"}
25 "coq-core" {= version}
26 "odoc" {with-doc}
27]
28depopts: ["coq-native"]
29dev-repo: "git+https://github.com/coq/coq.git"
30build: [
31 ["dune" "subst"] {dev}
32 # We tell dunestrap to use coq-config from coq-core
33 [ make "dunestrap" "COQ_DUNE_EXTRA_OPT=-split" "DUNESTRAPOPT=-p coq-stdlib"]
34 [
35 "dune"
36 "build"
37 "-p"
38 name
39 "-j"
40 jobs
41 "--promote-install-files=false"
42 "@install"
43 "@runtest" {with-test}
44 "@doc" {with-doc}
45 ]
46 ["dune" "install" "-p" name "--create-install-files" name]
47]
48
49url {
50 src: "https://github.com/coq/coq/releases/download/V8.20.0/coq-8.20.0.tar.gz"
51 checksum: [
52 "md5=66e57ea55275903bef74d5bf36fbe0f1"
53 "sha512=1a7eac6e2f58724a3f9d68bbb321e4cfe963ba1a5551b9b011db4b3f559c79be433d810ff262593d753770ee41ea68fbd6a60daa1e2319ea00dff64c8851d70b"
54 ]
55}