Dies ist der Befehl coqdep, der beim kostenlosen Hosting-Anbieter OnWorks mit einer unserer zahlreichen kostenlosen Online-Workstations wie Ubuntu Online, Fedora Online, dem Windows-Online-Emulator oder dem MAC OS-Online-Emulator ausgeführt werden kann
PROGRAMM:
NAME/FUNKTION
coqdep – Berechnen Sie Abhängigkeiten zwischen Modulen für Coq- und Caml-Programme
ZUSAMMENFASSUNG
coqdep [ -w ] [ -I Verzeichnis ] [ -coqlib Verzeichnis ] [ -c ] [ -i ] [ -D ] [ -Schrägstrich ]
Dateinamen ... Verzeichnis ...
BESCHREIBUNG
coqdep Berechnen Sie Abhängigkeiten zwischen Modulen für Coq- und Caml-Programme und drucken Sie die aus
Abhängigkeiten von der Standardausgabe in einem von make lesbaren Format. Wenn ein Verzeichnis ist
als Argument gegeben, wird es rekursiv betrachtet.
Abhängigkeiten von Coq-Modulen werden durch Betrachten berechnet Erfordern Befehle (Require, Require
Exportieren, Import erforderlich), Erklären ML Modul Befehle und Laden Sie Befehle. Abhängigkeiten
relativ zu Modulen aus der Coq-Bibliothek werden nicht gedruckt.
Abhängigkeiten von Caml-Modulen werden durch Betrachten berechnet XNUMXh geöffnet Direktiven und der Punkt
Notation module.value.
OPTIONAL
-c Druckt die Abhängigkeiten von Caml-Modulen. (Bei Caml-Modulen ist das Verhalten
genau das gleiche wie ocamldep).
-w Gibt eine Warnung aus, wenn ein Coq-Befehl vorliegt Erklären ML Modul ist falsch. (Zum Beispiel,
Sie haben „ML-Modul „A“ deklarieren“ geschrieben, aber das Modul A enthält #open „B“). Der
korrekter Befehl wird ausgegeben (siehe Option -D). Die Warnung ist standardmäßig aufgedruckt
Fehler.
-D Dieser Befehl sucht nach jedem Befehl Erklären ML Modul jeder Coq-Datei angegeben als
Argument und vervollständigen Sie (falls erforderlich) die Liste der Caml-Module. Der neue Befehl lautet
auf der Standardausgabe gedruckt. Mit dieser Option wird keine Abhängigkeit berechnet.
-Schrägstrich Druckt Pfade mit einem Schrägstrich anstelle des betriebssystemspezifischen Trennzeichens. Diese Option ist
nützlich bei der Entwicklung unter Cygwin.
-I Verzeichnis
Die Dateien .v .ml .mli des Verzeichnisses Verzeichnis werden dabei berücksichtigt
Berechnung von Abhängigkeiten, aber ihre eigenen Abhängigkeiten werden nicht gedruckt.
-coqlib Verzeichnis
Gibt an, wo sich die Coq-Bibliothek befindet. Der Standardwert wurde bei ermittelt
Installationszeit, daher sollte diese Option unter normalen Umständen nicht verwendet werden
Umstände.
Verwenden Sie coqdep online über die Dienste von onworks.net
