Paquet : coq (8.3.pl4+dfsg-1 et autres)

[ Paquet source : coq  ]

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.

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 package to be installed.

Étiquettes: Développement de logiciel: Compilateur, Domaine: Mathématiques, Mis en œuvre en: implemented-in::ocaml, interface::commandline, Interface utilisateur: Interactive en mode texte, Rôle: role::program, scope::utility, Boîte à outils d'interface utilisateur: Interface utilisateur texte ncurses

Autres paquets associés à coq

• dep: coq-libs (= 8.1.pl3+dfsg-1) [m68k]

  Paquet indisponible

• dep: coq-theories (= 8.2.pl2+dfsg-2) [hppa, powerpcspe]

  proof assistant for higher-order logic (theories)

  dep: coq-theories (= 8.3.pl2+dfsg-1) [sparc64]

  dep: coq-theories (= 8.3.pl4+dfsg-1) [non hppa, m68k, powerpcspe, sparc64]

• dep: emacsen-common

  code commun à toutes les versions d'Emacs

• dep: libc0.1 (>= 2.7) [kfreebsd-amd64, kfreebsd-i386]

  bibliothèque C GNU embarquée : bibliothèques partagées
  un paquet virtuel est également fourni par libc0.1-udeb

• dep: libc0.3 (>= 2.7) [hurd-i386]

  bibliothèque C GNU embarquée : bibliothèques partagées
  un paquet virtuel est également fourni par libc0.3-udeb

• dep: libc6 (>= 2.11) [powerpcspe]

  bibliothèque C GNU embarquée : bibliothèques partagées
  un paquet virtuel est également fourni par libc6-udeb

  dep: libc6 (>= 2.2) [hppa]

  dep: libc6 (>= 2.5-5) [m68k]

  dep: libc6 (>= 2.7) [amd64, armel, i386, powerpc, sparc]

• dep: libcoq-ocaml-ehg05 [armel]

  paquet virtuel fourni par libcoq-ocaml

• dep: libcoq-ocaml-m0xl3 [amd64, kfreebsd-amd64]

  paquet virtuel fourni par libcoq-ocaml

• dep: libcoq-ocaml-nc3h8 [alpha, armhf, ia64, mips, mipsel, s390, s390x, sh4]

  paquet virtuel fourni par libcoq-ocaml

• dep: libcoq-ocaml-rn5x5 [sparc64]

  paquet virtuel fourni par libcoq-ocaml

• dep: libcoq-ocaml-s00f5 [hurd-i386, i386, kfreebsd-i386, powerpc, sparc]

  paquet virtuel fourni par libcoq-ocaml

• dep: libgcc1 (>= 1:4.4.0) [armel]

  Bibliothèque de support GCC

• dep: libncurses5 (>= 5.6+20071006-3) [m68k]

  Bibliothèques partagées pour l'utilisation d'un terminal

• dep: ocaml-base-nox-3.10.2 [m68k]

  Paquet indisponible

• dep: ocaml-base-nox-3.11.2 [hppa, powerpcspe]

  paquet virtuel fourni par ocaml-base-nox

• dep: ocaml-base-nox-3.12.0 [sparc64]

  paquet virtuel fourni par ocaml-base-nox

• dep: ocaml-base-nox-3.12.1 [non hppa, m68k, powerpcspe, sparc64]

  paquet virtuel fourni par ocaml-base-nox

• dep: tex-common (>= 1.10) [m68k]

  infrastructure commune pour construire et installer TeX

• rec: coqide [non hppa, m68k, powerpcspe, sparc64]

  proof assistant for higher-order logic (gtk interface)

  ou proofgeneral

  generic frontend for proof assistants

• rec: coqide [hppa, m68k, powerpcspe, sparc64]

  proof assistant for higher-order logic (gtk interface)

  ou proofgeneral-coq

  interface générique pour les outils d'aide à la preuve - support de Coq

• sug: cle [m68k]

  Paquet indisponible

• sug: coq-doc

  documentation for Coq

• sug: ledit [m68k]

  éditeur de lignes pour les programmes interactifs

• sug: ledit [non m68k]

  éditeur de lignes pour les programmes interactifs

  ou readline-editor

  paquet virtuel fourni par ledit, rlfe, rlwrap

• sug: libcoq-ocaml-dev [non m68k]

  development libraries and tools for Coq

• sug: ocaml-nox [non m68k]

  Mise en oeuvre de Meta Language avec un système orienté objet (pas de X)

  sug: ocaml-nox (>= 3.08) [m68k]

• sug: proofgeneral [non hppa, m68k, powerpcspe, sparc64]

  generic frontend for proof assistants

• sug: proofgeneral-coq [hppa, m68k, powerpcspe, sparc64]

  interface générique pour les outils d'aide à la preuve - support de Coq

• sug: why (>= 2.19) [non m68k]

  Software verification tool

Télécharger coq

Télécharger pour toutes les architectures proposées

Architecture	Version	Taille du paquet	Espace occupé une fois installé	Fichiers
alpha (portage non officiel)	8.3.pl4+dfsg-1	1 769,9 ko	8 225,0 ko	[liste des fichiers]
amd64	8.3.pl4+dfsg-1	5 542,9 ko	18 432,0 ko	[liste des fichiers]
armel	8.3.pl4+dfsg-1	5 967,2 ko	17 898,0 ko	[liste des fichiers]
armhf	8.3.pl4+dfsg-1	1 770,7 ko	8 225,0 ko	[liste des fichiers]
hppa	8.2.pl2+dfsg-2	3 608,8 ko	18 268,0 ko	[liste des fichiers]
hurd-i386	8.3.pl4+dfsg-1+b1	4 941,7 ko	15 044,0 ko	[liste des fichiers]
i386	8.3.pl4+dfsg-1	4 946,3 ko	15 045,0 ko	[liste des fichiers]
ia64	8.3.pl4+dfsg-1+b1	1 770,0 ko	8 225,0 ko	[liste des fichiers]
kfreebsd-amd64	8.3.pl4+dfsg-1	5 537,4 ko	18 311,0 ko	[liste des fichiers]
kfreebsd-i386	8.3.pl4+dfsg-1	4 940,5 ko	14 925,0 ko	[liste des fichiers]
m68k (portage non officiel)	8.1.pl3+dfsg-1+b2	4 014,9 ko	18 580,0 ko	[liste des fichiers]
mips	8.3.pl4+dfsg-1	1 768,9 ko	8 225,0 ko	[liste des fichiers]
mipsel	8.3.pl4+dfsg-1+b1	1 768,6 ko	8 225,0 ko	[liste des fichiers]
powerpc	8.3.pl4+dfsg-1	5 427,1 ko	15 876,0 ko	[liste des fichiers]
powerpcspe (portage non officiel)	8.2.pl2+dfsg-2	3 606,8 ko	18 260,0 ko	[liste des fichiers]
s390	8.3.pl4+dfsg-1	1 770,0 ko	8 225,0 ko	[liste des fichiers]
s390x	8.3.pl4+dfsg-1	1 771,4 ko	8 225,0 ko	[liste des fichiers]
sh4 (portage non officiel)	8.3.pl4+dfsg-1	1 770,3 ko	8 225,0 ko	[liste des fichiers]
sparc	8.3.pl4+dfsg-1	5 289,9 ko	15 807,0 ko	[liste des fichiers]
sparc64 (portage non officiel)	8.3.pl2+dfsg-1	1 763,2 ko	8 432,0 ko	[liste des fichiers]