this repo has no description
anil.recoil.org
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
20depends: [
21 "ocaml" {>= "4.05.0" & < "4.10"}
22 "ocamlfind" {build}
23 "num"
24 "conf-findutils" {build}
25]
26depopts: [
27 "coq-native"
28]
29build: [
30 [
31 "./configure"
32 "-configdir" "%{lib}%/coq/config"
33 "-prefix" prefix
34 "-mandir" man
35 "-docdir" doc
36 "-libdir" "%{lib}%/coq"
37 "-datadir" "%{share}%/coq"
38 "-coqide" "no"
39 "-native-compiler" "yes" {coq-native:installed} "no" {!coq-native:installed}
40 ]
41 [make "-j%{jobs}%"]
42 [make "-j%{jobs}%" "byte"]
43]
44install: [
45 [make "install"]
46 [make "install-byte"]
47]
48
49url {
50 src: "https://github.com/coq/coq/releases/download/V8.11.0/coq-8.11.0.tar.gz"
51 checksum: "sha512=db7c3da4bab268cb729bcf9f03f5cd3bbb7a3b5b7094fe2b110189e54e436f9883640db88643d09cec5dc169c209a51661238e41b8de3035ff7ea8561c794c89"
52}
53extra-source "coq.install" {
54 src:
55 "https://raw.githubusercontent.com/ocaml/opam-source-archives/main/patches/coq/coq.install.8.11.0"
56 checksum:
57 "sha512=b501737b4dbd22adc1c0377d744448056fb1dc493caf72c05f57c8463cf23f758373605ab3a50b9f505e4c856c41039d0bd7f81f96ed62adc6a674179523e7d2"
58}