Paquet : coq (8.16.1+dfsg-1 et autres)

[ Paquet source : coq  ]

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

• dep: libc6 (>= 2.35)

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

• dep: libcoq-core-ocaml-4ew58 [armhf]

  paquet virtuel fourni par libcoq-core-ocaml

• dep: libcoq-core-ocaml-7k9u9 [s390x]

  paquet virtuel fourni par libcoq-core-ocaml

• dep: libcoq-core-ocaml-cpf60 [amd64]

  paquet virtuel fourni par libcoq-core-ocaml

• dep: libcoq-core-ocaml-cqbo5 [ppc64el]

  paquet virtuel fourni par libcoq-core-ocaml

• dep: libcoq-core-ocaml-cspq5 [i386]

  paquet virtuel fourni par libcoq-core-ocaml

• dep: libcoq-core-ocaml-wc485 [arm64]

  paquet virtuel fourni par libcoq-core-ocaml

• dep: libcoq-stdlib (= 8.16.1+dfsg-1+b2)

  outil d'aide à la preuve pour la logique d'ordre supérieur (théories)

• dep: libfindlib-ocaml-0thr1 [amd64]

  paquet virtuel fourni par libfindlib-ocaml

• dep: libfindlib-ocaml-3yei3 [armhf]

  paquet virtuel fourni par libfindlib-ocaml

• dep: libfindlib-ocaml-85sc9 [i386]

  paquet virtuel fourni par libfindlib-ocaml

• dep: libfindlib-ocaml-9bk70 [ppc64el]

  paquet virtuel fourni par libfindlib-ocaml

• dep: libfindlib-ocaml-dhcd7 [s390x]

  paquet virtuel fourni par libfindlib-ocaml

• dep: libfindlib-ocaml-unji9 [arm64]

  paquet virtuel fourni par libfindlib-ocaml

• dep: libgmp10 (>= 2:6.2.1+dfsg1)

  Bibliothèque arithmétique à multi-précision

• dep: libzarith-ocaml-4dps0 [amd64, arm64, ppc64el]

  paquet virtuel fourni par libzarith-ocaml

• dep: libzarith-ocaml-aip06 [armhf, i386]

  paquet virtuel fourni par libzarith-ocaml

• dep: libzarith-ocaml-vtl52 [s390x]

  paquet virtuel fourni par libzarith-ocaml

• dep: ocaml-base-4.13.1

  paquet virtuel fourni par ocaml-base

• dep: ocaml-findlib

  management tool for OCaml libraries

• dep: ocaml-nox

  paquet de transition pour ocaml

• dep: python3

  interactive high-level object-oriented language (default python3 version)

• sug: coq-doc

  documentation for Coq

• 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-core-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.16.1+dfsg-1+b2	91 027,9 ko	352 732,0 ko	[liste des fichiers]
arm64	8.16.1+dfsg-1+b2	99 773,5 ko	398 315,0 ko	[liste des fichiers]
armhf	8.16.1+dfsg-1+b2	87 761,3 ko	286 184,0 ko	[liste des fichiers]
i386	8.16.1+dfsg-1+b2	85 466,2 ko	312 470,0 ko	[liste des fichiers]
ppc64el	8.16.1+dfsg-1+b2	91 686,3 ko	372 982,0 ko	[liste des fichiers]
s390x	8.16.1+dfsg-1+b2	91 127,8 ko	375 279,0 ko	[liste des fichiers]