Questo è il comando coqchk.opt che può essere eseguito nel provider di hosting gratuito OnWorks utilizzando una delle nostre molteplici workstation online gratuite come Ubuntu Online, Fedora Online, emulatore online Windows o emulatore online MAC OS
PROGRAMMA:
NOME
coqchk - Il verificatore di librerie compilate Coq Proof Checker
SINOSSI
coqchk [ Opzioni ] moduli
DESCRIZIONE
coqchk è il controllo autonomo delle librerie compilate (file .vo prodotti da coqc) per
il Coq Proof Assistant. Consultare il Manuale di riferimento per ulteriori informazioni. Ritorna con
codice di uscita 0 se tutte le attività richieste sono riuscite. Un codice di ritorno diverso da zero significa che
qualcosa è andato storto: qualche libreria non è stata trovata, contenuto danneggiato, controllo del tipo
fallimento, ecc.
moduli è un elenco di moduli da controllare. I moduli possono essere indicati con un breve o
nome qualificato.
VERSIONI
-I dire, --includere dir
aggiungi directory dir nel percorso di inclusione
-R dir coqdir
mappare ricorsivamente fisica dir a logico coqdir
-silenzioso
rende coqchk meno prolisso.
-ammettere modulo
contrassegna il modulo specificato e tutte le sue dipendenze come attendibili e non lo sarà
ricontrollato, a meno che non sia esplicitamente richiesto da altre opzioni.
-norec modulo
specifica che il modulo dato deve essere verificato senza richiedere di verificarne
dipendenze.
-M, --memoria
visualizza un riepilogo della memoria utilizzata dal correttore.
-oh, --contesto-output
visualizza un riepilogo del contenuto logico verificato: ipotesi e
uso dell'impredicatività.
-insieme-impredicativo
consente al correttore di accettare librerie che sono state compilate con questo flag.
-v stampa la versione coqchk ed esci.
-coqlib dir
sovrascrive la posizione predefinita della libreria standard.
-dove stampa la posizione della libreria standard coqchk ed esci.
-H, --Aiuto
stampa l'elenco delle opzioni
Usa coqchk.opt online utilizzando i servizi onworks.net
