this repo has no description
anil.recoil.org
1# This file is generated by dune, edit dune-project instead
2opam-version: "2.0"
3synopsis: "The Coq Proof Assistant -- Core Binaries and Tools"
4description: """
5Coq is a formal proof management system. It provides
6a formal language to write mathematical definitions, executable
7algorithms and theorems together with an environment for
8semi-interactive development of machine-checked proofs.
9
10Typical applications include the certification of properties of
11programming languages (e.g. the CompCert compiler certification
12project, or the Bedrock verified low-level programming library), the
13formalization of mathematics (e.g. the full formalization of the
14Feit-Thompson theorem or homotopy type theory) and teaching.
15
16This package includes the Coq core binaries, plugins, and tools, but
17not the vernacular standard library.
18
19Note that in this setup, Coq needs to be started with the -boot and
20-noinit options, as will otherwise fail to find the regular Coq
21prelude, now living in the coq-stdlib package."""
22maintainer: ["The Coq development team <coqdev@inria.fr>"]
23authors: ["The Coq development team, INRIA, CNRS, and contributors"]
24license: "LGPL-2.1-only"
25homepage: "https://coq.inria.fr/"
26doc: "https://coq.github.io/doc/"
27bug-reports: "https://github.com/coq/coq/issues"
28depends: [
29 "dune" {>= "2.9"}
30 "ocaml" {>= "4.09.0"}
31 "ocamlfind" {>= "1.8.1"}
32 "zarith" {>= "1.11"}
33 "ounit2" {with-test}
34]
35conflicts: [
36 "coq" { < "8.17" }
37 "ocaml-variants" {= "4.12.0+domains+effects" | = "5.1.1+effect-syntax"}
38 "ocaml-compiler" {= "5.3.0~alpha1"}
39]
40build-env: OCAMLPARAM = "_,w=-46,warn-error=-a,keywords=5.2"
41build: [
42 # Requires dune 2.8 due to https://github.com/ocaml/dune/issues/3219
43 # ["dune" "subst"] {pinned}
44 [ "./configure"
45 "-prefix" prefix
46 "-mandir" man
47 "-libdir" "%{lib}%/coq"
48 "-native-compiler" "yes" {coq-native:installed} "no" {!coq-native:installed}
49 ]
50 [
51 "dune"
52 "build"
53 "-p"
54 name
55 "-j"
56 jobs
57 "@install"
58 "@runtest" {with-test}
59 "@doc" {with-doc}
60 ]
61]
62dev-repo: "git+https://github.com/coq/coq.git"
63depopts: ["coq-native"]
64url {
65 src:
66 "https://github.com/coq/coq/releases/download/V8.18.0/coq-8.18.0.tar.gz"
67 checksum: [
68 "md5=8d852367b54f095d9fbabd000304d450"
69 "sha512=46922d5f2eb6802a148a52fd3e7f0be8370c93e7bc33cee05cf4a2044290845b10ccddbaa306f29c808e7c5019700763e37e45ff6deb507b874a4348010fed50"
70 ]
71}