coqdoc - Online in der Cloud

PROGRAMM:

NAME/FUNKTION

coqdoc - Ein Dokumentationstool für den Coq-Proof-Assistenten

ZUSAMMENFASSUNG

coqdoc [ Optionen ] Dateien

BESCHREIBUNG

coqdoc ist ein Dokumentationstool für den Coq-Proof-Assistenten. Es erstellt LaTeX oder HTML
Dokumente aus einer Reihe von Coq-Dateien. Dokumentation finden Sie im Coq-Referenzhandbuch (URL
unten).

OPTIONAL

Insgesamt: Optionen
-h Hilfe. Gibt Ihnen die vollständige Liste der von coqdoc akzeptierten Optionen.

--html Wählen Sie eine HTML-Ausgabe aus.

--Latex
Wählen Sie einen LATEX-Ausgang.

--dvi Wählen Sie einen DVI-Ausgang aus.

--ps Wählen Sie eine PostScript-Ausgabe aus.

--texmacs
Wählen Sie eine TeXmacs-Ausgabe aus.

--stdout
Leiten Sie die Ausgabe auf stdout um

-o Datei,--Ausgabe Datei
Leiten Sie die Ausgabe in die Datei um Datei.

-d ist, --Verzeichnis dir
Dateien in Verzeichnis ausgeben dir anstelle des aktuellen Verzeichnisses (Option -d nicht
den mit der Option -o angegebenen Dateinamen ändern, falls vorhanden).

-S, --kurz
Fügen Sie keine Titel für die Dateien ein. Das Standardverhalten ist das Einfügen eines Titels wie
``Library Foo'' für jede Datei.

-t Schnur --Titel Schnur
Legen Sie den Dokumenttitel fest.

--nur Körper
Unterdrücken Sie die Kopfzeile und den Trailer des endgültigen Dokuments. So können Sie die
resultierende Dokument in ein größeres.

-p Schnur --Präambel Schnur
Fügen Sie etwas Material in die LATEX-Präambel ein, direkt vor \begin{document}
(bedeutungslos mit -html).

--vernac-Datei Datei, --tex-Datei Datei
Betrachtet die Datei `file' jeweils als .v (oder .g) Datei oder als .tex Datei.

--Dateien-von Datei
Lesen Sie die Dateinamen, die in der Datei `file' verarbeitet werden sollen, als ob sie auf dem Befehl angegeben wurden
Leitung. Nützlich für Programmquellen, die in mehrere Verzeichnisse aufgeteilt sind.

-Q, --ruhig
Ruhig sein. Drucken Sie nichts außer Fehlern.

-H, --help
Geben Sie eine kurze Zusammenfassung der Optionen und beenden Sie den Vorgang.

-in, --Version
Version drucken und beenden.

Index Optionen
Das Standardverhalten besteht darin, einen Index nur für die HTML-Ausgabe in index.html zu erstellen.

--no-index
Geben Sie den Index nicht aus.

--multi-index
Generieren Sie eine Seite für jede Kategorie und jeden Buchstaben im Index, zusammen mit a
Hauptseite index.html.

Tisch of Inhalt zu erhalten
-toc, --Inhaltsverzeichnis
Fügen Sie ein Inhaltsverzeichnis ein. Für eine LATEX-Ausgabe fügt es ein \tableofcontents at . ein
der Anfang des Dokuments. Für eine HTML-Ausgabe erstellt es ein Inhaltsverzeichnis
in toc.html.

Hyperlinks Optionen
--glob-von Datei
Erstellen Sie Referenzen mithilfe von Coq-Globalisierungen aus der Dateidatei. (Solche Globalisierungen sind
erhalten mit der Coq-Option -dump-glob).

--keine-externen
Fügen Sie keine Links zur Coq-Standardbibliothek ein.

--extern URL libroot
Legen Sie die Basis-URL für die externe Bibliothek fest, deren Root-Präfix libroot ist.

--coqlib URL
Basis-URL für die Coq-Standardbibliothek festlegen (Standard ist
http://coq.inria.fr/library/).

--coqlib_path dir
Legen Sie den Basispfad fest, in dem die Coq-Dateien installiert werden, insbesondere die Stildateien
coqdoc.sty und coqdoc.css.

-R dir coqdir
Ordnen Sie das physische Verzeichnis dir dem logischen Coq-Verzeichnis coqdir zu (ähnlich der Coq-Option
-R). Hinweis: Option -R wirkt sich nur auf die Dateien aus, die ihr auf den Befehl folgen
line, daher müssen Sie diese Option wahrscheinlich zuerst setzen.

Inhalte Optionen
-G, - Gallina
Drucken Sie keine Probeabzüge.

- l, --hell
Lichtmodus. Unterdrücke Beweise (wie bei -g) und die folgenden Befehle:

* [rekursive] Taktikdefinition
* Hinweis / Hinweise
* Benötigen
* Transparent / Undurchsichtig
* Implizites Argument / Implizite
* Abschnitt / Variable / Hypothese / Ende

Das Verhalten der Optionen -g und -l kann lokal mit dem (* begin show
*) ... (* Show beenden *) Umgebung (siehe oben).

Sprache Optionen
Das Standardverhalten besteht darin, ASCII 7-Bit-Eingabedateien anzunehmen.

-lateinisch1, --latin1
Wählen Sie ISO-8859-1-Eingabedateien aus. Es entspricht --inputenc latin1 --charset
ISO-8859-1.

-utf8, --utf8
Wählen Sie UTF-8 (Unicode)-Eingabedateien aus. Es entspricht --inputenc utf8 --charset
utf-8. LATEX UTF-8-Unterstützung finden Sie unter
http://www.ctan.org/tex-archive/macros/latex/contrib/supported/unicode/.

--inputenc Schnur
Geben Sie dem LATEX-Paket inputenc optional eine LATEX-Eingabekodierung.

--Zeichensatz Schnur
Geben Sie den HTML-Zeichensatz an, der in den HTML-Header eingefügt werden soll.

Verwenden Sie coqdoc online mit den onworks.net-Diensten