Il s'agit de la commande coqchk 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
coqchk - Le vérificateur de bibliothèques compilées Coq Proof Checker
SYNOPSIS
coqchk [ Options ] modules
DESCRIPTION
coqchk est le vérificateur autonome des bibliothèques compilées (fichiers .vo produits par coqc) pour
l'assistant de preuve Coq. Consultez le Manuel de référence pour plus d'informations. Il revient avec
code de sortie 0 si toutes les tâches demandées ont réussi. Un code retour différent de zéro signifie que
quelque chose s'est mal passé : une bibliothèque n'a pas été trouvée, contenu corrompu, vérification de type
échec, etc.
modules est une liste de modules à vérifier. Les modules peuvent être désignés par une courte ou
nom qualifié.
OPTIONS
-I d, --comprendre dir
ajouter un répertoire dir dans le chemin d'inclusion
-R dir coqdir
mapper récursivement physique dir logique coqdir
-silencieux
rend coqchk moins verbeux.
-admettre module
marquer le module spécifié et toutes ses dépendances comme étant de confiance, et ne sera pas
revérifié, sauf si explicitement demandé par d'autres options.
-norec module
spécifie que le module donné doit être vérifié sans demander de vérifier son
dépendances.
-m, --Mémoire
affiche un résumé de la mémoire utilisée par le vérificateur.
-o, --contexte-de-sortie
affiche un résumé du contenu logique qui a été vérifié : hypothèses et
usage de l'imprédicativité.
-ensemble-imprédicatif
permet au vérificateur d'accepter les bibliothèques qui ont été compilées avec ce drapeau.
-v imprimer la version coqchk et quitter.
-coqlib dir
remplace l'emplacement par défaut de la bibliothèque standard.
-où imprimez l'emplacement de la bibliothèque standard coqchk et quittez.
-h, --Aidez-moi
imprimer la liste des options
Utilisez coqchk en ligne en utilisant les services onworks.net
