Il s'agit de la commande coqtop qui peut être exécutée dans le fournisseur d'hébergement gratuit OnWorks en utilisant l'un de nos multiples postes de travail en ligne gratuits tels que Ubuntu Online, Fedora Online, l'émulateur en ligne Windows ou l'émulateur en ligne MAC OS
PROGRAMME:
Nom
coqtop - Le système de haut niveau Coq Proof Assistant
SYNOPSIS
coq [ Options ]
DESCRIPTION
coq est le système de premier niveau de Coq, pour une utilisation interactive. Il lit des phrases sur le
entrée standard et imprime les résultats sur la sortie standard.
Pour une utilisation par lots de Coq, voir coqc (1).
OPTIONS
-h, --Aidez-moi
Aider. Vous donnera la liste complète des options acceptées par coqtop.
-I d, --comprendre dir
ajouter un répertoire dir dans le chemin d'inclusion
-R dir coqdir
mapper récursivement physique dir logique coqdir
-Haut coqdir
définir le nom de niveau supérieur comme coqdir au lieu de Haut
-état d'entrée nom de fichier, -is nom de fichier
lire l'état du fichier nom de fichier.coq
-bruit commencer avec un état initial vide
-état de sortienom de fichier
écrire l'état dans le fichier nom de fichier.coq
-load-ml-objet nom de fichier
charger le fichier objet ML nom de fichier
-load-ml-source nom de fichier
charger le fichier ML nom de fichier
-charge-vernac-source nom de fichier, -l nom de fichier
charger le fichier Coq nom de fichier.v (Charger le nom de fichier.)
-load-vernac-source-verbeux nom de fichier, -nv nom de fichier
charger en détail le fichier Coq nom de fichier.v (Charger le nom de fichier détaillé.)
-load-vernac-objet nom de fichier
charger le fichier objet Coq nom de fichier.vo
-exiger nom de fichier
charger le fichier objet Coq nom de fichier.vo et importez-le (Require Import filename.)
-compiler nom de fichier
compiler le fichier Coq nom de fichier.v (implique -grouper )
-compiler-verbeux nom de fichier
compiler en détail le fichier Coq nom de fichier.v (implique -grouper )
-opter exécuter la version en code natif de Coq
-octet exécuter la version bytecode de Coq
-où imprimer l'emplacement de la bibliothèque standard de Coq et quitter
-v imprimer la version Coq et quitter
-q ignorer le chargement du fichier rc
-fichier-init nom de fichier
définir le fichier rc sur nom de fichier
-grouper mode batch (quitte juste après l'analyse des arguments)
-démarrage mode de démarrage (implique -q et -grouper )
-emacs dit à Coq qu'il est exécuté sous Emacs
-dump-glob nom de fichier
dump des globalisations dans le fichier f (à utiliser par coqdoc(1) )
-avec-geoproof (oui|non)
pour (dés)activer des fonctions spéciales pour Geoproof dans Coqide (la valeur par défaut est oui )
-ensemble-imprédicatif
set sort Set imprédicatif
-ne-chargez-preuves
ne charge pas les épreuves opaques en mémoire
-xml exporter des fichiers XML soit vers la hiérarchie ancrée dans le répertoire
$COQ_XML_LIBRARY_ROOT (si défini) ou vers stdout (si désactivé)
Qualité
améliorer la lisibilité des termes de preuve produits par certaines tactiques
Utiliser coqtop en ligne en utilisant les services onworks.net
