this repo has no description
1opam-version: "2.0"
2synopsis: "The Coq Proof Assistant"
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."""
14maintainer: ["The Coq development team <coqdev@inria.fr>"]
15authors: ["The Coq development team, INRIA, CNRS, and contributors"]
16license: "LGPL-2.1-only"
17homepage: "https://coq.inria.fr/"
18doc: "https://coq.github.io/doc/"
19bug-reports: "https://github.com/coq/coq/issues"
20depends: [
21 "dune" {>= "2.9"}
22 "coq-core" {= version}
23 "coq-stdlib" {= version}
24 "coqide-server" {= version}
25]
26build: [
27 ["dune" "subst"] {dev}
28 [
29 "dune"
30 "build"
31 "-p"
32 name
33 "-j"
34 jobs
35 "@install"
36 "@runtest" {with-test}
37 "@doc" {with-doc}
38 ]
39]
40dev-repo: "git+https://github.com/coq/coq.git"
41
42url {
43 src: "https://github.com/coq/coq/releases/download/V8.17.0/coq-8.17.0.tar.gz"
44 checksum: "sha512=2f77bcb5211018b5d46320fd39fd34450eeb654aca44551b28bb50a2364398c4b34587630b6558db867ecfb63b246fd3e29dc2375f99967ff62bc002db9c3250"
45}