Questo è il comando coqide 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
coqide - L'interfaccia grafica di Coq Proof Assistant
SINOSSI
coqide [ Opzioni ]
DESCRIZIONE
coqide è un'interfaccia grafica gtk per l'assistente di prova Coq.
Per l'uso orientato alla riga di comando di Coq, vedere coqtop(1) ; per l'uso orientato ai batch di Coq, vedere
coqc(1).
VERSIONI
-h Mostra l'elenco completo delle opzioni accettate da coqide.
-I dir, -includere dir
Aggiungi directory dir nel percorso di inclusione.
-R dir coqdir
Mappa ricorsivamente fisico dir a logico coqdir.
-sorgente Aggiungi le directory di origine nel percorso di inclusione.
-è f, -stato di ingresso f
Leggi lo stato da f.coq.
-rumore Inizia con uno stato vuoto.
-stato di uscita f
Scrivi lo stato nel file f.coq.
-load-ml-oggetto f
Carica file oggetto ML f.
-load-ml-sorgente f
Carica file ML f.
-l f, -load-vernac-source f
Carica file Coq f.v (Carica f.).
-liv f, -load-vernac-source-verbose f
Carica file Coq f.v (Carica Verbose f.).
-load-vernac-oggetto f
Carica file oggetto Coq f.vo.
-richiedere f
Carica file oggetto Coq f.vo e importalo (Richiedi f.).
-compilare f
Compila il file Coq f.v (implica -lotto).
-compilare-verbose f
Compila in modo dettagliato il file Coq f.v (implica -lotto).
-optare Eseguire la versione in codice nativo di Coq o Coq_SearchIsos.
-byte Eseguire la versione bytecode di Coq o Coq_SearchIsos.
-dove Stampa la posizione della libreria standard di Coq ed esci.
-v Stampa la versione Coq ed esci.
-q Salta il caricamento di rcfile.
-file-init f
Imposta il file rc su f.
-lotto Modalità batch (esce subito dopo l'analisi degli argomenti).
-stivale Modalità di avvio (implica -q ed -lotto).
-emac Dice a Coq che viene eseguito sotto Emacs.
-glob di scarico f
Scarica le globalizzazioni nel file f (da usare da coqdoc(1)).
-insieme-impredicativo
Imposta ordinamento Imposta impredicativo.
-non-caricare-prove
Non caricare prove opache in memoria.
-xml Esporta i file XML nella gerarchia radicata nella directory
COQ_XML_LIBRARY_ROOT (se impostato) o su stdout (se non impostato).
Usa coqide online utilizzando i servizi onworks.net
