Il s'agit de la commande coqdep 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
coqdep - Calculer les dépendances inter-modules pour les programmes Coq et Caml
SYNOPSIS
coqdep [ -w ] [ -I annuaire ] [ -coqlib annuaire ] [ -c ] [ -i ] [ -D ] [ -sabrer ]
nom de fichier annuaire
DESCRIPTION
coqdep calcule les dépendances inter-modules pour les programmes Coq et Caml, et imprime le
dépendances sur la sortie standard dans un format lisible par make. Lorsqu'un répertoire est
donnée comme argument, elle est regardée récursivement.
Les dépendances des modules Coq sont calculées en regardant Exiger commandes (Exiger, Exiger
Exporter, Exiger une importation), Déclarer ML Module commandes et Charge commandes. Dépendances
relatifs aux modules de la bibliothèque Coq ne sont pas imprimés.
Les dépendances des modules Caml sont calculées en regardant ouvert directives et le point
notation module.valeur.
OPTIONS
-c Imprime les dépendances des modules Caml. (Sur les modules Caml, le comportement est
exactement le même que ocamldep).
-w Imprime un avertissement si une commande Coq Déclarer ML Module est incorrect. (Par exemple,
vous avez écrit `Declare ML Module "A".', mais le module A contient #open "B"). Les
la commande correcte est imprimée (voir l'option -D). L'avertissement est imprimé sur la norme
Erreur.
-D Cette commande recherche chaque commande Déclarer ML Module de chaque fichier Coq donné comme
argument et complétez (si besoin) la liste des modules Caml. La nouvelle commande est
imprimé sur la sortie standard. Aucune dépendance n'est calculée avec cette option.
-sabrer Imprime les chemins en utilisant une barre oblique au lieu du séparateur spécifique au système d'exploitation. Cette option est
utile lors du développement sous Cygwin.
-I annuaire
Les fichiers .v .ml .mli du répertoire annuaire sont pris en compte lors de la
calcul des dépendances, mais leurs propres dépendances ne sont pas imprimées.
-coqlib annuaire
Indique où se trouve la bibliothèque Coq. La valeur par défaut a été déterminée à
temps d'installation, et par conséquent cette option ne doit pas être utilisée dans des conditions normales
circonstances.
Utiliser coqdep en ligne en utilisant les services onworks.net
