Aceasta este comanda coqdep care poate fi rulată în furnizorul de găzduire gratuit OnWorks folosind una dintre multiplele noastre stații de lucru online gratuite, cum ar fi Ubuntu Online, Fedora Online, emulator online Windows sau emulator online MAC OS
PROGRAM:
NUME
coqdep - Calculați dependențe între module pentru programele Coq și Caml
REZUMAT
coqdep [ -w ] [ -I director ] [ -coqlib director ] [ -c ] [ -i ] [ -D ] [ -bară oblică ]
nume de fișier ... director ...
DESCRIERE
coqdep calculează dependențele dintre module pentru programele Coq și Caml și tipărește fișierul
dependențe de ieșirea standard într-un format care poate fi citit de make. Când un director este
dat ca argument, este privit recursiv.
Dependențe ale modulelor Coq sunt calculate privind Necesita comenzi (Require, Require
Export, necesită import), Declara ML Module comenzi și A incarca comenzi. Dependente
relativ la modulele din biblioteca Coq nu sunt tipărite.
Dependențe ale modulelor Caml sunt calculate privind deschide directivele și punctul
notaţie modul.valoare.
OPŢIUNI
-c Imprimă dependențele modulelor Caml. (Pe modulele Caml, comportamentul este
exact la fel ca ocamldep).
-w Imprimă un avertisment dacă o comandă Coq Declara ML Module este incorect. (De exemplu,
ați scris `Declare ML Module "A".', dar modulul A conține #open "B"). The
comanda corectă este tipărită (vezi opțiunea -D). Avertismentul este tipărit standard
eroare.
-D Această comandă caută fiecare comandă Declara ML Module din fiecare fișier Coq dat ca
argumentați și completați (dacă este necesar) lista modulelor Caml. Noua comandă este
tipărit pe ieşirea standard. Nu se calculează nicio dependență cu această opțiune.
-bară oblică Imprimă căile folosind o bară oblică în loc de separatorul specific pentru sistemul de operare. Această opțiune este
util atunci când se dezvoltă sub Cygwin.
-I director
Fișierele .v .ml .mli ale directorului director sunt luate în considerare în timpul
calculul dependențelor, dar propriile dependențe nu sunt tipărite.
-coqlib director
Indică unde se află biblioteca Coq. Valoarea implicită a fost determinată la
timpul de instalare și, prin urmare, această opțiune nu ar trebui utilizată în condiții normale
circumstanțe.
Utilizați coqdep online folosind serviciile onworks.net
