[ Paquet source : coq ]
Paquet : coq (8.20.1+dfsg-1 et autres)
Liens pour coq
Ressources Debian :
- Rapports de bogues
- Developer Information
- Journal des modifications Debian
- Fichier de licence
- Suivis des correctifs pour Debian
Télécharger le paquet source coq :
Responsables :
- Debian OCaml Maintainers (Page QA, Archive du courrier électronique)
- Benjamin Barenblat (Page QA)
- Julien Puydt (Page QA)
- Ralf Treinen (Page QA)
- Stéphane Glondu (Page QA)
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é.
Autres paquets associés à coq
|
|
|
|
-
- dep: coq-libs (= 8.1.pl3+dfsg-1) [m68k]
- Paquet indisponible
-
- dep: coq-theories (= 8.12.0-3+b3) [alpha, hppa, ia64, sh4, sparc64, x32]
- outil d'aide à la preuve pour la logique d'ordre supérieur (théories)
-
- dep: emacsen-common [m68k]
- code commun à toutes les versions d'Emacs
-
- dep: libc6 (>= 2.38) [amd64, arm64, ppc64, ppc64el, riscv64, s390x]
- bibliothèque C GNU : bibliothèques partagées
un paquet virtuel est également fourni par libc6-udeb
- dep: libc6 (>= 2.39) [loong64]
- dep: libc6 (>= 2.5-5) [m68k]
-
- dep: libcoq-core-ocaml-7yf86 [s390x]
- paquet virtuel fourni par libcoq-core-ocaml
-
- dep: libcoq-core-ocaml-ajzi5 [arm64]
- paquet virtuel fourni par libcoq-core-ocaml
-
- dep: libcoq-core-ocaml-at3u5 [amd64]
- paquet virtuel fourni par libcoq-core-ocaml
-
- dep: libcoq-core-ocaml-d2hd1 [loong64]
- paquet virtuel fourni par libcoq-core-ocaml
-
- dep: libcoq-core-ocaml-k4nx1 [ppc64el]
- paquet virtuel fourni par libcoq-core-ocaml
-
- dep: libcoq-core-ocaml-t2147 [riscv64]
- paquet virtuel fourni par libcoq-core-ocaml
-
- dep: libcoq-core-ocaml-yi844 [ppc64]
- paquet virtuel fourni par libcoq-core-ocaml
-
- dep: libcoq-ocaml-4s3g2 [alpha, hppa, ia64, sh4, sparc64, x32]
- paquet virtuel fourni par libcoq-ocaml
-
- dep: libcoq-stdlib (= 8.19.1+dfsg-3) [loong64, ppc64]
- outil d'aide à la preuve pour la logique d'ordre supérieur (théories)
- dep: libcoq-stdlib (= 8.20.1+dfsg-1) [amd64, arm64, ppc64el, riscv64, s390x]
-
- dep: libfindlib-ocaml-5dit4 [arm64]
- paquet virtuel fourni par libfindlib-ocaml
-
- dep: libfindlib-ocaml-9a346 [s390x]
- paquet virtuel fourni par libfindlib-ocaml
-
- dep: libfindlib-ocaml-l8hb7 [ppc64]
- Paquet indisponible
-
- dep: libfindlib-ocaml-o8mp7 [ppc64el]
- paquet virtuel fourni par libfindlib-ocaml
-
- dep: libfindlib-ocaml-t0ap1 [loong64]
- Paquet indisponible
-
- dep: libfindlib-ocaml-t4zk4 [riscv64]
- paquet virtuel fourni par libfindlib-ocaml
-
- dep: libfindlib-ocaml-xdxk1 [amd64]
- paquet virtuel fourni par libfindlib-ocaml
-
- dep: libgmp10 (>= 2:6.3.0+dfsg) [amd64, arm64, loong64, ppc64, ppc64el, riscv64, s390x]
- Bibliothèque arithmétique à multi-précision
-
- dep: libncurses5 (>= 5.6+20071006-3) [m68k]
- Paquet indisponible
-
- dep: libnum-ocaml-3st20 [alpha, hppa, ia64, sh4, sparc64, x32]
- paquet virtuel fourni par libnum-ocaml
-
- dep: libstdlib-ocaml-fxjy5 [amd64, arm64, ppc64el, riscv64]
- paquet virtuel fourni par libstdlib-ocaml
-
- dep: libstdlib-ocaml-gats1 [ppc64]
- Paquet indisponible
-
- dep: libstdlib-ocaml-ke4j9 [s390x]
- paquet virtuel fourni par libstdlib-ocaml
-
- dep: libstdlib-ocaml-vyp69 [loong64]
- Paquet indisponible
-
- dep: libzarith-ocaml-avzf2 [ppc64]
- Paquet indisponible
-
- dep: libzarith-ocaml-f1se9 [amd64, arm64, ppc64el, riscv64]
- paquet virtuel fourni par libzarith-ocaml
-
- dep: libzarith-ocaml-i2hh0 [s390x]
- paquet virtuel fourni par libzarith-ocaml
-
- dep: libzarith-ocaml-zlfv4 [loong64]
- Paquet indisponible
-
- dep: ocaml [amd64, arm64, loong64, ppc64, ppc64el, riscv64, s390x]
- mise en oeuvre de Meta Language avec un système orienté objet basé sur les classes
-
- dep: ocaml-base-4.14.1 [loong64, ppc64]
- paquet virtuel fourni par ocaml-base
-
- dep: ocaml-base-5.3.0 [amd64, arm64, ppc64el, riscv64, s390x]
- paquet virtuel fourni par ocaml-base
-
- dep: ocaml-base-nox-3.10.2 [m68k]
- Paquet indisponible
-
- dep: ocaml-base-nox-4.11.1 [alpha, hppa, ia64, sh4, sparc64, x32]
- Paquet indisponible
-
- dep: ocaml-findlib [non m68k]
- management tool for OCaml libraries
-
- dep: ocaml-nox [alpha, hppa, ia64, sh4, sparc64, x32]
- paquet de transition pour ocaml
-
- dep: python3 [non m68k]
- langage orienté objet interactif de haut niveau – version par défaut de Python 3
-
- dep: tex-common (>= 1.10) [m68k]
- infrastructure commune pour construire et installer TeX
-
- rec: coqide
- outil d'aide à la preuve pour la logique d'ordre supérieur (interface en GTK)
- ou proofgeneral-coq
- Paquet indisponible
-
- sug: cle [m68k]
- Paquet indisponible
-
- sug: coq-doc
- documentation for Coq
-
- sug: coqide [non m68k]
- 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 [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-core-ocaml-dev [amd64, arm64, loong64, ppc64, ppc64el, riscv64, s390x]
- development libraries and tools for Coq
-
- sug: libcoq-ocaml-dev [alpha, hppa, ia64, sh4, sparc64, x32]
- development libraries and tools for Coq
-
- sug: ocaml-nox (>= 3.08) [m68k]
- paquet de transition pour ocaml
-
- sug: proofgeneral-coq [m68k]
- Paquet indisponible
-
- sug: why (>= 2.19) [non m68k]
- Paquet indisponible
Télécharger coq
| Architecture | Version | Taille du paquet | Espace occupé une fois installé | Fichiers |
|---|---|---|---|---|
| alpha (portage non officiel) | 8.12.0-3+b3 | 103 380,6 ko | 412 882,0 ko | [liste des fichiers] |
| amd64 | 8.20.1+dfsg-1 | 68 574,8 ko | 255 831,0 ko | [liste des fichiers] |
| arm64 | 8.20.1+dfsg-1 | 72 692,7 ko | 277 363,0 ko | [liste des fichiers] |
| hppa (portage non officiel) | 8.12.0-3+b3 | 103 393,2 ko | 412 952,0 ko | [liste des fichiers] |
| ia64 (portage non officiel) | 8.12.0-3+b3 | 103 379,1 ko | 412 878,0 ko | [liste des fichiers] |
| loong64 (portage non officiel) | 8.19.1+dfsg-3 | 82 879,7 ko | 330 249,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] |
| ppc64 (portage non officiel) | 8.19.1+dfsg-3 | 80 065,5 ko | 339 636,0 ko | [liste des fichiers] |
| ppc64el | 8.20.1+dfsg-1 | 69 187,4 ko | 266 936,0 ko | [liste des fichiers] |
| riscv64 | 8.20.1+dfsg-1 | 69 527,1 ko | 266 346,0 ko | [liste des fichiers] |
| s390x | 8.20.1+dfsg-1 | 69 405,7 ko | 274 877,0 ko | [liste des fichiers] |
| sh4 (portage non officiel) | 8.12.0-3+b3 | 103 401,4 ko | 412 954,0 ko | [liste des fichiers] |
| sparc64 (portage non officiel) | 8.12.0-3+b3 | 103 374,8 ko | 412 882,0 ko | [liste des fichiers] |
| x32 (portage non officiel) | 8.12.0-3+b3 | 103 397,8 ko | 412 954,0 ko | [liste des fichiers] |