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 "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.19.0/coq-8.19.0.tar.gz"
51 checksum: [
52 "md5=64b49dbc3205477bd7517642c0b9cbb6"
53 "sha512=02fb5b4fb575af79e092492cbec6dc0d15a1d74a07f827f657a72d4e6066532630e5a6d15be4acdb73314bd40b9a321f9ea0584e0ccfe51fd3a56353bd30db9b"
54 ]
55}