Il s'agit de la commande coqide.byte 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
coqide - L'interface graphique de Coq Proof Assistant
SYNOPSIS
coqide [ Options ]
DESCRIPTION
coqide est une interface graphique gtk pour l'assistant de preuve Coq.
Pour une utilisation en ligne de commande de Coq, voir coq(1) ; pour l'utilisation par lots de Coq, voir
coqc (1).
OPTIONS
-h Afficher la liste complète des options acceptées par coqide.
-I dir, -comprendre dir
Ajoutez le répertoire dir dans le chemin d'inclusion.
-R dir coqdir
Mapper récursivement le physique dir logique coqdir.
-src Ajoutez des répertoires source dans le chemin d'inclusion.
-is f, -état d'entrée f
Lire l'état de f.coq.
-bruit Commencez avec un état vide.
-état de sortie f
Écrire l'état dans le fichier f.coq.
-load-ml-objet f
Charger le fichier objet ML f.
-load-ml-source f
Charger le fichier ML f.
-l f, -charge-vernac-source f
Charger le fichier Coq f.v (Charger f.).
-lv f, -load-vernac-source-verbeux f
Charger le fichier Coq f.v (Charger le verbeux f.).
-load-vernac-objet f
Charger le fichier objet Coq f.vo.
-exiger f
Charger le fichier objet Coq f.vo et importez-le (nécessite f.).
-compiler f
Compiler le fichier Coq f.v (implique -grouper).
-compiler-verbeux f
Compiler en détail le fichier Coq f.v (implique -grouper).
-opter Exécutez la version en code natif de Coq ou Coq_SearchIsos.
-octet Exécutez la version bytecode de Coq ou Coq_SearchIsos.
-où Imprimez l'emplacement standard de la bibliothèque de Coq et quittez.
-v Imprimer la version Coq et quitter.
-q Ignorer le chargement du fichier rc.
-fichier-init f
Définissez le fichier rc sur f.
-grouper Mode batch (quitte juste après l'analyse des arguments).
-démarrage Mode de démarrage (implique -q et -grouper).
-emacs Indique à Coq qu'il est exécuté sous Emacs.
-dump-glob f
Vider les globalisations dans le fichier f (à utiliser par coqdoc(1)).
-ensemble-imprédicatif
Set sort Set imprédicatif.
-ne-chargez-preuves
Ne chargez pas d'épreuves opaques en mémoire.
-xml Exporter les fichiers XML soit vers la hiérarchie ancrée dans le répertoire
COQ_XML_LIBRARY_ROOT (si défini) ou sur stdout (si désactivé).
Utilisez coqide.byte en ligne en utilisant les services onworks.net
