File: control

package info (click to toggle)
coq 8.9.0-1
  • links: PTS, VCS
  • area: main
  • in suites: bullseye, buster, sid
  • size: 30,604 kB
  • sloc: ml: 192,230; sh: 2,585; python: 2,206; ansic: 1,878; makefile: 818; lisp: 202; xml: 24; sed: 2
file content (108 lines) | stat: -rw-r--r-- 3,361 bytes parent folder | download
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
Source: coq
Section: math
Priority: optional
Maintainer: Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>
Uploaders:
 Benjamin Barenblat <bbaren@debian.org>,
 Ralf Treinen <treinen@debian.org>,
 Samuel Mimram <smimram@debian.org>,
 St├ęphane Glondu <glondu@debian.org>,
 Enrico Tassi <gareuselesinge@debian.org>
Standards-Version: 4.3.0
Build-Depends:
 debhelper (>= 10),
 dh-exec,
 dh-ocaml (>= 0.9.5~),
 dh-python,
 ocaml-nox (>= 4.02.3),
 ocaml-findlib (>= 1.4.1),
 camlp5 (>= 6.14),
 liblablgtk2-ocaml-dev (>= 2.14),
 liblablgtksourceview2-ocaml-dev,
 libounit-ocaml-dev,
 python3,
 rsync,
 texlive-latex-extra,
 hevea (>= 1.10-7)
Homepage: http://coq.inria.fr/
Vcs-Browser: https://salsa.debian.org/ocaml-team/coq
Vcs-Git: https://salsa.debian.org/ocaml-team/coq.git

Package: coq
Architecture: any
Depends:
 coq-theories (= ${binary:Version}),
 ${ocaml:Depends},
 ${python3:Depends},
 ${shlibs:Depends},
 ${misc:Depends}, 
 ocaml-nox,
 ocaml-findlib
Provides: coq-${F:CoqABI}
Suggests:
 proofgeneral,
 ledit | readline-editor,
 libcoq-ocaml-dev,
 why (>= 2.19),
 coq-doc
Breaks: coq-libs (<< 8.2.pl1)
Replaces: coq-libs (<< 8.2.pl1)
Description: proof assistant for higher-order logic (toplevel and compiler)
 Coq is a proof assistant for higher-order logic, which allows the
 development of computer programs consistent with their formal
 specification. It is developed using Objective Caml and Camlp5.
 .
 This package provides coqtop, a command line interface to Coq.
 .
 The proofgeneral package allows proofs to be edited using Emacs and
 XEmacs.

Package: coq-theories
Architecture: any
Depends: coq-${F:CoqABI}, ${misc:Depends}, ${shlibs:Depends}
Recommends: coq (>= 8.0)
Breaks: coq-doc (<= 8.0pl1.0-2), coq-libs (<< 8.2.pl1)
Replaces: coq-libs (<< 8.2.pl1)
Description: proof assistant for higher-order logic (theories)
 Coq is a proof assistant for higher-order logic, which allows the
 development of computer programs consistent with their formal
 specification. It is developed using Objective Caml and Camlp5.
 .
 This package provides existing theories that new proofs can be
 based upon, including theories of arithmetic and Boolean values.

Package: libcoq-ocaml
Section: ocaml
Architecture: any
Depends:
 ${ocaml:Depends},
 ${shlibs:Depends},
 ${misc:Depends}
Provides: ${ocaml:Provides}
Breaks: coq (<< 8.3~), libcoq-ocaml-dev (<< 8.3~), coq-libs
Replaces: coq (<< 8.3~), libcoq-ocaml-dev (<< 8.3~), coq-libs
Description: runtime libraries for Coq
 Coq is a proof assistant for higher-order logic, which allows the
 development of computer programs consistent with their formal
 specification. It is developed using Objective Caml and Camlp5.
 .
 This package provides runtime libraries for Coq.

Package: libcoq-ocaml-dev
Section: ocaml
Architecture: any
Depends:
 coq (= ${binary:Version}),
 ${ocaml:Depends},
 ${shlibs:Depends},
 ${misc:Depends}
Provides: ${ocaml:Provides}
Breaks: coq (<< 8.2-1+dfsg-1), coq-libs (<< 8.2.pl1)
Replaces: coq (<< 8.2-1+dfsg-1), coq-libs (<< 8.2.pl1)
Description: development libraries and tools for Coq
 Coq is a proof assistant for higher-order logic, which allows the
 development of computer programs consistent with their formal
 specification. It is developed using Objective Caml and Camlp5.
 .
 This package provides and libraries needed to develop OCaml-side
 extensions to Coq.