coqdoc - Online in de cloud

PROGRAMMA:

NAAM

coqdoc - Een documentatietool voor de Coq proof-assistent

KORTE INHOUD

coqdoc [ opties ] bestanden

PRODUCTBESCHRIJVING

coqdoc is een documentatietool voor de Coq proof-assistent. Het maakt LaTeX of HTML
documenten uit een set Coq-bestanden. Zie de Coq-referentiehandleiding voor documentatie (url
hieronder).

OPTIES

globaal opties
-h Helpen. Geeft u de volledige lijst met opties die door coqdoc worden geaccepteerd.

--html Selecteer een HTML-uitvoer.

--latex
Selecteer een LATEX-uitgang.

--dvi Selecteer een DVI-uitgang.

- Selecteer een PostScript-uitvoer.

--texmacs
Selecteer een TeXmacs-uitvoer.

--stdout
Leid de uitvoer om naar stdout

-o bestand--uitvoer filet
Leid de uitvoer om naar het bestand bestand.

-d richt, --map dir
Bestanden uitvoeren naar directory dir in plaats van de huidige map (optie -d niet
verander de bestandsnaam gespecificeerd met optie -o, indien aanwezig).

-Ja, --kort
Voeg geen titels voor de bestanden in. Het standaardgedrag is om een ​​titel in te voegen zoals
``Bibliotheek Foo'' voor elk bestand.

-t draad, --titel snaar
Stel de documenttitel in.

--alleen lichamelijk
Onderdruk de header en trailer van het uiteindelijke document. Zo kunt u de
resulterend document in een groter document.

-p draad, --preambule snaar
Plaats wat materiaal in de LATEX-preambule, vlak voor \begin{document}
(betekenisloos met -html).

--vernac-bestand bestand --tex-bestand filet
Beschouwt het bestand `bestand' respectievelijk als een .v (of .g) bestand of een .tex bestand.

--bestanden-van filet
Lees bestandsnamen om in bestand `bestand' te verwerken alsof ze op de opdracht zijn gegeven
lijn. Handig voor programmabronnen die in verschillende mappen zijn opgesplitst.

-Q, --stil
Wees stil. Druk niets af, behalve fouten.

-H, --help
Geef een korte samenvatting van de opties en sluit af.

-in, --versie
Print de versie en sluit af.

Index opties
Het standaardgedrag is het bouwen van een index, alleen voor de HTML-uitvoer, in index.html.

--geen-index
Voer de index niet uit.

--multi-index
Genereer één pagina voor elke categorie en elke letter in de index, samen met a
toppagina index.html.

tafel of inhoud optie
-tok, --inhoudsopgave
Voeg een inhoudsopgave toe. Voor een LATEX-uitvoer voegt het een \tabel met inhoud toe aan
het begin van het document. Voor een HTML-uitvoer bouwt het een inhoudsopgave
in toc.html.

hyperlinks opties
--glob-van filet
Maak referenties met behulp van Coq-globaliseringen uit het bestandsbestand. (Dergelijke globaliseringen zijn
verkregen met Coq-optie -dump-glob).

--geen-externen
Plaats geen links naar de Coq-standaardbibliotheek.

--extern url liroot
Stel de basis-URL in voor de externe bibliotheek waarvan het root-voorvoegsel libroot is.

--coqlib url
Stel de basis-URL in voor de Coq-standaardbibliotheek (standaard is
http://coq.inria.fr/library/).

--coqlib_pad dir
Stel het basispad in waar de Coq-bestanden worden geïnstalleerd, met name stijlbestanden
coqdoc.sty en coqdoc.css.

-R dir coqdir
Wijs fysieke map dir toe aan Coq logische map coqdir (vergelijkbaar met Coq optie
-R). Opmerking: optie -R heeft alleen effect op de bestanden die erop volgen op het commando
regel, dus u zult deze optie waarschijnlijk eerst moeten plaatsen.

Inhoud opties
-G, --gallina
Druk geen proefdrukken af.

-ik, --licht
Lichte modus. Onderdruk bewijzen (zoals bij -g) en de volgende commando's:

* [Recursieve] tactiekdefinitie
* Tip / tips
* Vereisen
* Transparant / ondoorzichtig
* Impliciete Argumenten / Implicieten
* Sectie / Variabele / Hypothese / Einde

Het gedrag van de opties -g en -l kan lokaal worden overschreven met de (* begin show
*) ... (*einde show *) omgeving (zie hierboven).

Taal opties
Het standaardgedrag is om ASCII 7-bits invoerbestanden aan te nemen.

-latijn1, --latijn1
Selecteer ISO-8859-1 invoerbestanden. Het is gelijk aan --inputenc latin1 --charset
iso-8859-1.

-utf8, --utf8
Selecteer UTF-8 (Unicode) invoerbestanden. Het is gelijk aan --inputenc utf8 --charset
utf-8. LATEX UTF-8-ondersteuning is te vinden op:
http://www.ctan.org/tex-archive/macros/latex/contrib/supported/unicode/.

--input snaar
Geef een LATEX-invoercodering als optie aan LATEX-pakket inputenc.

--tekenset snaar
Geef de HTML-tekenset op die in de HTML-header moet worden ingevoegd.

Gebruik coqdoc online met onworks.net-services