this repo has no description
anil.recoil.org
1opam-version: "2.0"
2synopsis: "The Coq Proof Assistant -- Core Binaries and Tools"
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 core binaries, plugins, and tools, but
16not the vernacular standard library.
17
18Note that in this setup, Coq needs to be started with the -boot and
19-noinit options, as will otherwise fail to find the regular Coq
20prelude, now living in the coq-stdlib package."""
21maintainer: ["The Coq development team <coqdev@inria.fr>"]
22authors: ["The Coq development team, INRIA, CNRS, and contributors"]
23license: "LGPL-2.1-only"
24homepage: "https://coq.inria.fr/"
25doc: "https://coq.github.io/doc/"
26bug-reports: "https://github.com/coq/coq/issues"
27depends: [
28 "dune" {>= "2.9"}
29 "ocaml" {>= "4.09.0"}
30 "ocamlfind" {>= "1.8.1"}
31 "zarith" {>= "1.11"}
32 "ounit2" {with-test}
33]
34conflicts: [
35 "coq" { < "8.17" }
36 "ocaml-variants" {= "4.12.0+domains+effects" | = "5.1.1+effect-syntax"}
37 "ocaml-compiler" {= "5.3.0~alpha1"}
38]
39build-env: OCAMLPARAM = "_,w=-46,warn-error=-a,keywords=5.2"
40build: [
41 [ "./configure"
42 "-prefix" prefix
43 "-mandir" man
44 "-libdir" "%{lib}%/coq"
45 "-native-compiler" "yes" {coq-native:installed} "no" {!coq-native:installed}
46 ]
47 [
48 "dune"
49 "build"
50 "-p"
51 name
52 "-j"
53 jobs
54 "@install"
55 "@runtest" {with-test}
56 "@doc" {with-doc}
57 ]
58]
59dev-repo: "git+https://github.com/coq/coq.git"
60depopts: ["coq-native"]
61
62url {
63 src: "https://github.com/coq/coq/releases/download/V8.17.1/coq-8.17.1.tar.gz"
64 checksum: "sha512=9a35311acec2a806730b94ac7dceabc88837f235c52a14c026827d9b89433bd7fa9555a9fc6829aa49edfedb24c8bbaf1411ebf463b74a50aeb17cba47745b6b"
65}