Paquet : coq (8.12.0-3 et autres)

Liens pour coq

Ressources Debian :

Télécharger le paquet source coq :

Responsables :

Ressources externes :

Page d'accueil [coq.inria.fr]

Paquets similaires :

outil d'aide à la preuve pour la logique d'ordre supérieur (environnement interactif et compilateur)

Coq est un assistant de preuve pour la logique d'ordre supérieur, qui permet le développement de programmes d'ordinateur correspondant à une spécification formelle. Il est développé en Objective Caml et Camlp5.

Ce paquet fournit coqtop, une interface en ligne de commande pour Coq.

Une interface graphique pour Coq est fournie dans le paquet coqide. On peut aussi utiliser Coq avec ProofGeneral, qui permet l'édition de preuves dans Emacs et XEmacs. Pour cela, le paquet proofgeneral doit être installé.

É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

dépendances

recommandations

suggestions

enhances

dep: coq-theories (= 8.12.0-3+b3)

outil d'aide à la preuve pour la logique d'ordre supérieur (théories)
dep: libc6 (>= 2.29) [non armel, mips64el, mipsel]

bibliothèque C GNU : bibliothèques partagées
un paquet virtuel est également fourni par libc6-udeb
dep: libcoq-ocaml-1fwg6 [ppc64el]

paquet virtuel fourni par libcoq-ocaml
dep: libcoq-ocaml-4pem8 [arm64]

paquet virtuel fourni par libcoq-ocaml
dep: libcoq-ocaml-4s3g2 [armel, mips64el, mipsel]

paquet virtuel fourni par libcoq-ocaml
dep: libcoq-ocaml-otko2 [i386]

paquet virtuel fourni par libcoq-ocaml
dep: libcoq-ocaml-xs455 [amd64]

paquet virtuel fourni par libcoq-ocaml
dep: libcoq-ocaml-zuzr9 [armhf]

paquet virtuel fourni par libcoq-ocaml
dep: libnum-ocaml-3st20 [armel, mips64el, mipsel]

paquet virtuel fourni par libnum-ocaml
dep: libnum-ocaml-80ki3 [amd64, arm64, ppc64el]

paquet virtuel fourni par libnum-ocaml
dep: libnum-ocaml-hqq52 [armhf, i386]

paquet virtuel fourni par libnum-ocaml
dep: ocaml-base-nox-4.11.1

paquet virtuel fourni par ocaml-base-nox
dep: ocaml-findlib

management tool for OCaml libraries
dep: ocaml-nox

mise en œuvre de Meta Language avec un système orienté objet (pas de X)
dep: python3

langage orienté objet interactif de haut niveau – version par défaut de Python 3

sug: coq-doc

Paquet indisponible
sug: coqide

outil d'aide à la preuve pour la logique d'ordre supérieur (interface en GTK)

ou proofgeneral

frontal générique d’assistants de preuve
sug: ledit

éditeur de lignes pour les programmes interactifs

ou readline-editor

paquet virtuel fourni par ledit, rlfe, rlwrap
sug: libcoq-ocaml-dev

development libraries and tools for Coq
sug: why (>= 2.19)

Paquet indisponible

Télécharger coq

Télécharger pour toutes les architectures proposées
Architecture	Version	Taille du paquet	Espace occupé une fois installé	Fichiers
amd64	8.12.0-3+b3	88 333,2 ko	358 108,0 ko	[liste des fichiers]
arm64	8.12.0-3+b3	93 820,2 ko	384 451,0 ko	[liste des fichiers]
armel	8.12.0-3+b3	103 391,0 ko	412 954,0 ko	[liste des fichiers]
armhf	8.12.0-3+b3	86 284,5 ko	308 733,0 ko	[liste des fichiers]
i386	8.12.0-3+b3	85 826,4 ko	329 208,0 ko	[liste des fichiers]
mips64el	8.12.0-3+b3	103 385,3 ko	412 882,0 ko	[liste des fichiers]
mipsel	8.12.0-3+b3	103 402,0 ko	412 954,0 ko	[liste des fichiers]
ppc64el	8.12.0-3+b3	89 332,1 ko	371 137,0 ko	[liste des fichiers]