Englishfrançaisespagnol

Icône de favori OnWorks

coqdep - En ligne dans le Cloud

Exécutez coqdep dans le fournisseur d'hébergement gratuit OnWorks sur Ubuntu Online, Fedora Online, l'émulateur en ligne Windows ou l'émulateur en ligne MAC OS

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


Serveurs et postes de travail gratuits

Télécharger des applications Windows et Linux

  • 1
    frapper
    frapper
    Projet de logiciel libre Strikr. Artefacts
    publié sous un « intent based »
    double licence : AGPLv3 (communauté) et
    CC-BY-NC-ND 4.0 international
    (commercial)...
    Télécharger
  • 3
    GIFLIB
    GIFLIB
    giflib est une bibliothèque pour lire et
    écrire des images gif. C'est API et ABI
    compatible avec libungif qui était dans
    large utilisation tandis que la compression LZW
    l'algorithme était...
    Télécharger GIFLIB
  • 4
    Alt+F
    Alt+F
    Alt-F fournit une source libre et ouverte
    firmware alternatif pour le DLINK
    DNS-320/320L/321/323/325/327L and
    DNR-322L. Alt-F a Samba et NFS ;
    prend en charge ext2/3/4...
    Télécharger Alt-F
  • 5
    usm
    usm
    Usm est un package slackware unifié
    gestionnaire qui gère automatique
    résolution de dépendance. Il unifie
    divers référentiels de packages, y compris
    slackware, slacky, p...
    Télécharger usm
  • 6
    Chart.js
    Chart.js
    Chart.js est une bibliothèque Javascript qui
    permet aux concepteurs et aux développeurs de dessiner
    toutes sortes de graphiques utilisant le HTML5
    élément de toile. Chart js offre un excellent
    déployer ...
    Télécharger Chart.js
  • Plus "

Commandes Linux

Ad