Aceasta este comanda coqchk.opt 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
coqchk - Verificatorul de biblioteci compilat Coq Proof Checker
REZUMAT
coqchk [ Opțiuni ] module
DESCRIERE
coqchk este verificatorul independent al bibliotecilor compilate (fișiere .vo produse de coqc) pentru
asistentul Coq Proof. Consultați Manualul de referință pentru mai multe informații. Se intoarce cu
codul de ieșire 0 dacă toate sarcinile solicitate au reușit. Un cod de returnare diferit de zero înseamnă că
ceva a mers prost: o bibliotecă nu a fost găsită, conținut corupt, verificare de tip
eșec etc.
module este o listă de module care trebuie verificate. Modulele pot fi menționate printr-un scurt sau
nume calificat.
OPŢIUNI
-I este, --include dir
adaugă directorul dir în calea include
-R dir coqdir
mapează recursiv fizic dir la logic coqdir
-tăcut
face coqchk mai puțin verbos.
-recunosc modul
etichetați modulul specificat și toate dependențele sale ca fiind de încredere și nu vor fi
verificat din nou, cu excepția cazului în care este solicitat în mod explicit de alte opțiuni.
-norec modul
specifică faptul că modulul dat va fi verificat fără a solicita verificarea acestuia
dependențe.
-m, --memorie
afișează un rezumat al memoriei utilizate de verificator.
-o, --output-context
afişează un rezumat al conţinutului logic care a fost verificat: ipoteze şi
utilizarea impredicativității.
-impredicative-set
permite verificatorului să accepte biblioteci care au fost compilate cu acest flag.
-v tipăriți versiunea coqchk și ieșiți.
-coqlib dir
suprascrie locația implicită a bibliotecii standard.
-Unde tipăriți locația bibliotecii standard coqchk și ieșiți.
-h, --Ajutor
tipăriți lista de opțiuni
Utilizați coqchk.opt online folosind serviciile onworks.net
