this repo has no description
1opam-version: "2.0"
2maintainer: "coqdev@inria.fr"
3authors: "The Coq development team, INRIA, CNRS, and contributors."
4homepage: "https://coq.inria.fr/"
5bug-reports: "https://github.com/coq/coq/issues"
6dev-repo: "git+https://github.com/coq/coq.git"
7license: "LGPL-2.1-only"
8synopsis: "Formal proof management system"
9description: """
10The Coq proof assistant provides a formal language to write
11mathematical definitions, executable algorithms, and theorems, together
12with an environment for semi-interactive development of machine-checked
13proofs. Typical applications include the certification of properties of programming
14languages (e.g., the CompCert compiler certification project and the
15Bedrock verified low-level programming library), the formalization of
16mathematics (e.g., the full formalization of the Feit-Thompson theorem
17and homotopy type theory) and teaching.
18"""
19
20depopts: [
21 "coq-native"
22]
23depends: [
24 "ocaml" {>= "4.05.0"}
25 "ocamlfind" {build}
26 "dune" {>= "2.5.1"}
27 "conf-findutils" {build}
28 "zarith" {>= "1.10"}
29]
30conflicts: [
31 "base-nnp"
32 "ocaml-option-nnpchecker"
33]
34build: [
35 [
36 "./configure"
37 "-configdir" "%{lib}%/coq/config"
38 "-prefix" prefix
39 "-mandir" man
40 "-docdir" "%{doc}%/coq"
41 "-libdir" "%{lib}%/coq"
42 "-datadir" "%{share}%/coq"
43 "-coqide" "no"
44 "-native-compiler" "yes" {coq-native:installed} "no" {!coq-native:installed}
45 ]
46 [ make "COQ_USE_DUNE=" "-j%{jobs}%" ]
47]
48install: [
49 [ make "COQ_USE_DUNE=" "install" ]
50]
51
52patches: [ "dune-install-set-root.patch" "ld_stricter.patch" "disable_warn_70.patch" ]
53
54url {
55 src: "https://github.com/coq/coq/releases/download/V8.14.0/coq-8.14.0.tar.gz"
56 checksum: "sha256=b1501d686c21836302191ae30f610cca57fb309214c126518ca009363ad2cd3c"
57}
58extra-source "ld_stricter.patch" {
59 src:
60 "https://raw.githubusercontent.com/ocaml/opam-source-archives/main/patches/coq/ld_stricter.patch"
61 checksum:
62 "sha256=a5cd1fe65889bb908e1194c37de428266b422f6040b5d729611eb100f054b591"
63}
64extra-source "dune-install-set-root.patch" {
65 src:
66 "https://raw.githubusercontent.com/ocaml/opam-source-archives/main/patches/coq/dune-install-set-root.patch"
67 checksum:
68 "sha256=e3071578fdddc45873fdc78446b1044c3ba8b1031bd05bbc901234cc1ebcceba"
69}
70extra-source "disable_warn_70.patch" {
71 src:
72 "https://raw.githubusercontent.com/ocaml/opam-source-archives/main/patches/coq/disable_warn_70.patch.8.14.0"
73 checksum:
74 "sha256=b305336e5103be6540519e6e6b67178e825f998c0f691553c2be1b5abb5a507d"
75}