diff options
Diffstat (limited to 'debian/control')
| -rw-r--r-- | debian/control | 59 |
1 files changed, 59 insertions, 0 deletions
diff --git a/debian/control b/debian/control new file mode 100644 index 00000000..6df245e8 --- /dev/null +++ b/debian/control @@ -0,0 +1,59 @@ +Source: coq +Section: math +Priority: optional +Maintainer: Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org> +Uploaders: Ralf Treinen <treinen@debian.org>, + Remi Vanicat <vanicat@debian.org>, + Stefano Zacchiroli <zack@debian.org>, + Samuel Mimram <smimram@debian.org>, + Stephane Glondu <steph@glondu.net> +DM-Upload-Allowed: yes +Standards-Version: 3.8.0 +Build-Depends: debhelper (>= 4.0.0), dpkg-dev (>= 1.13.19), dpatch, ocaml-nox (>= 3.10), ocaml-best-compilers, camlp5, liblablgtk2-ocaml-dev (>= 2.4.0), texlive-latex-extra, hevea +Homepage: http://coq.inria.fr/ +Vcs-Browser: http://git.debian.org/?p=pkg-ocaml-maint/packages/coq.git +Vcs-Git: git://git.debian.org/git/pkg-ocaml-maint/packages/coq.git + +Package: coq +Architecture: any +Depends: ${shlibs:Depends}, ${misc:Depends}, ocaml-base-nox-${F:OCamlABI}, coq-libs (= ${source:Version}), emacsen-common +Recommends: coqide | proofgeneral-coq +Suggests: ocaml-nox (>= 3.08), proofgeneral-coq, ledit, cle, coq-doc +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 Camlp4. + For more information, see <http://coq.inria.fr/>. + . + This packages provides coqtop, a command line interface to Coq. + . + A graphical interface for Coq is provided in the coqide package. + Coq can also be used with ProofGeneral, which allows proofs to be + edited using emacs and xemacs. This requires the proofgeneral-coq + package to be installed. + +Package: coqide +Architecture: any +Depends: ${shlibs:Depends}, ${misc:Depends}, coq (>= 8.0) +Description: proof assistant for higher-order logic (gtk interface) + 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 Camlp4. + For more information, see <http://coq.inria.fr/>. + . + This package provides CoqIde, a graphical user interface for + developing proofs. + +Package: coq-libs +Architecture: all +Depends: ${misc:Depends} +Recommends: coq (>= 8.0) +Conflicts: coq (<< 8.0), coq-doc (<= 8.0pl1.0-2) +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 Camlp4. + For more information, see <http://coq.inria.fr/>. + . + This package provides existing theories that new proofs can be + based upon, including theories of arithmetic and Boolean values. |