1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
|
(lang dune 3.6)
(name coq)
; We use directory targets in documentation
(using directory-targets 0.1)
; We need this due to `(coq.pp )` declarations
(using coq 0.6)
(formatting
(enabled_for ocaml))
(generate_opam_files true)
(license LGPL-2.1-only)
(maintainers "The Coq development team <coqdev@inria.fr>")
(authors "The Coq development team, INRIA, CNRS, and contributors")
; This generates bug-reports and dev-repo
(source (github coq/coq))
(homepage https://coq.inria.fr/)
(documentation "https://coq.github.io/doc/")
(version dev)
; Note that we use coq.opam.template to have dune add the correct opam
; prefix for configure; also note that we manually add the dune >= 3.6.1
; dependency due a dune bug preventing Coq to build in
; 3.6.0. Dune adds `dune >= 3.6` automatically, based on `(lang dune 3.6)`
; above, but that's not enough.
(package
(name coq-core)
(depends
(dune (>= 3.6.1))
(ocaml (>= 4.09.0))
(ocamlfind (>= 1.8.1))
(zarith (>= 1.11))
(conf-linux-libc-dev (= :os "linux")))
(depopts coq-native memprof-limits memtrace)
(synopsis "The Coq Proof Assistant -- Core Binaries and Tools")
(description "Coq is a formal proof management system. It provides
a formal language to write mathematical definitions, executable
algorithms and theorems together with an environment for
semi-interactive development of machine-checked proofs.
Typical applications include the certification of properties of
programming languages (e.g. the CompCert compiler certification
project, or the Bedrock verified low-level programming library), the
formalization of mathematics (e.g. the full formalization of the
Feit-Thompson theorem or homotopy type theory) and teaching.
This package includes the Coq core binaries, plugins, and tools, but
not the vernacular standard library.
Note that in this setup, Coq needs to be started with the -boot and
-noinit options, as will otherwise fail to find the regular Coq
prelude, now living in the coq-stdlib package."))
(package
(name coq-stdlib)
(depends
(coq-core (= :version)))
(depopts coq-native)
(synopsis "The Coq Proof Assistant -- Standard Library")
(description "Coq is a formal proof management system. It provides
a formal language to write mathematical definitions, executable
algorithms and theorems together with an environment for
semi-interactive development of machine-checked proofs.
Typical applications include the certification of properties of
programming languages (e.g. the CompCert compiler certification
project, or the Bedrock verified low-level programming library), the
formalization of mathematics (e.g. the full formalization of the
Feit-Thompson theorem or homotopy type theory) and teaching.
This package includes the Coq Standard Library, that is to say, the
set of modules usually bound to the Coq.* namespace."))
(package
(name coqide-server)
(depends
(coq-core (= :version)))
(synopsis "The Coq Proof Assistant, XML protocol server")
(description "Coq is a formal proof management system. It provides
a formal language to write mathematical definitions, executable
algorithms and theorems together with an environment for
semi-interactive development of machine-checked proofs.
This package provides the `coqidetop` language server, an
implementation of Coq's [XML protocol](https://github.com/coq/coq/blob/master/dev/doc/xml-protocol.md)
which allows clients, such as CoqIDE, to interact with Coq in a
structured way."))
(package
(name coqide)
(depends
(ocamlfind :build)
(conf-findutils :build)
conf-adwaita-icon-theme
(coqide-server (= :version))
(cairo2 (>= 0.6.4))
(lablgtk3-sourceview3 (and (>= 3.1.2) (or (>= 3.1.5) (<> :os "windows")))))
(synopsis "The Coq Proof Assistant --- GTK3 IDE")
(description "Coq is a formal proof management system. It provides
a formal language to write mathematical definitions, executable
algorithms and theorems together with an environment for
semi-interactive development of machine-checked proofs.
This package provides the CoqIDE, a graphical user interface for the
development of interactive proofs."))
(package
(name coq-doc)
(license "OPUBL-1.0")
(depends
(conf-python-3 :build)
(coq (and :build (= :version))))
(synopsis "The Coq Proof Assistant --- Reference Manual")
(description "Coq is a formal proof management system. It provides
a formal language to write mathematical definitions, executable
algorithms and theorems together with an environment for
semi-interactive development of machine-checked proofs.
This package provides the Coq Reference Manual."))
(package
(name coq)
(depends
(coq-core (= :version))
(coq-stdlib (= :version))
(coqide-server (= :version))
(ounit2 :with-test)
(conf-python-3 :with-test)
(conf-time :with-test))
(synopsis "The Coq Proof Assistant")
(description "Coq is a formal proof management system. It provides
a formal language to write mathematical definitions, executable
algorithms and theorems together with an environment for
semi-interactive development of machine-checked proofs.
Typical applications include the certification of properties of
programming languages (e.g. the CompCert compiler certification
project, or the Bedrock verified low-level programming library), the
formalization of mathematics (e.g. the full formalization of the
Feit-Thompson theorem or homotopy type theory) and teaching."))
|
