···
2
+
maintainer: "coqdev@inria.fr"
3
+
authors: "The Coq development team, INRIA, CNRS, and contributors."
4
+
homepage: "https://coq.inria.fr/"
5
+
bug-reports: "https://github.com/coq/coq/issues"
6
+
dev-repo: "git+https://github.com/coq/coq.git"
7
+
license: "LGPL-2.1-only"
8
+
synopsis: "Formal proof management system"
10
+
The Coq proof assistant provides a formal language to write
11
+
mathematical definitions, executable algorithms, and theorems, together
12
+
with an environment for semi-interactive development of machine-checked
13
+
proofs. Typical applications include the certification of properties of programming
14
+
languages (e.g., the CompCert compiler certification project and the
15
+
Bedrock verified low-level programming library), the formalization of
16
+
mathematics (e.g., the full formalization of the Feit-Thompson theorem
17
+
and homotopy type theory) and teaching.
24
+
"ocaml" {>= "4.05.0"}
27
+
"conf-findutils" {build}
28
+
"zarith" {>= "1.10"}
32
+
"ocaml-option-nnpchecker"
37
+
"-configdir" "%{lib}%/coq/config"
40
+
"-docdir" "%{doc}%/coq"
41
+
"-libdir" "%{lib}%/coq"
42
+
"-datadir" "%{share}%/coq"
44
+
"-native-compiler" "yes" {coq-native:installed} "no" {!coq-native:installed}
46
+
[ make "COQ_USE_DUNE=" "-j%{jobs}%" ]
49
+
[ make "COQ_USE_DUNE=" "install" ]
53
+
src: "https://github.com/coq/coq/archive/refs/tags/V8.15.0.tar.gz"
54
+
checksum: "sha256=73466e61f229b23b4daffdd964be72bd7a110963b9d84bd4a86bb05c5dc19ef3"