coqdoc - Online în cloud

PROGRAM:

NUME

coqdoc - Un instrument de documentare pentru asistentul Coq proof

REZUMAT

coqdoc [ Opțiuni ] fișiere

DESCRIERE

coqdoc este un instrument de documentare pentru asistentul Coq proof. Acesta creează LaTeX sau HTML
documente dintr-un set de fișiere Coq. Consultați manualul de referință Coq pentru documentație (url
de mai jos).

OPŢIUNI

Salopete Opțiuni
-h Ajutor. Vă va oferi lista completă a opțiunilor acceptate de coqdoc.

--html Selectați o ieșire HTML.

--latex
Selectați o ieșire LATEX.

--dvi Selectați o ieșire DVI.

--ps Selectați o ieșire PostScript.

--texmacs
Selectați o ieșire TeXmacs.

--stdout
Redirecționează ieșirea către stdout

-o fişier,--ieșire fişier
Redirecționați rezultatul în fișier fișier.

-d este, --director dir
Ieșiți fișierele în director dir în loc de directorul curent (opțiunea -d nu
schimbați numele fișierului specificat cu opțiunea -o, dacă există).

-da, --mic de statura
Nu introduceți titluri pentru fișiere. Comportamentul implicit este inserarea unui titlu ca
``Library Foo'' pentru fiecare fișier.

-t şir, --titlu şir
Setați titlul documentului.

--doar corp
Suprimați antetul și trailerul documentului final. Astfel, puteți introduce
documentul rezultat într-unul mai mare.

-p şir, --preambul şir
Introduceți ceva material în preambulul LATEX, chiar înainte de \begin{document}
(fără sens cu -html).

--vernac-file fişier, --tex-file fişier
Consideră fișierul „fișier”, respectiv ca un fișier .v (sau .g) sau un fișier .tex.

--fișiere-de la fişier
Citiți numele fișierelor pentru a fi procesate în fișierul „fișier” ca și cum ar fi fost date în comandă
linia. Util pentru sursele de programe împărțite în mai multe directoare.

-q, --Liniște
Liniște. Nu tipăriți nimic în afară de erori.

-h, --Ajutor
Oferiți un scurt rezumat al opțiunilor și ieșiți.

-v, --versiune
Imprimați versiunea și ieșiți.

index Opțiuni
Comportamentul implicit este de a construi un index, numai pentru ieșirea HTML, în index.html.

--fără-index
Nu scoateți indexul.

--multi-index
Generați câte o pagină pentru fiecare categorie și fiecare literă din index, împreună cu a
pagina de sus index.html.

Tabel of conținut opțiune
-toc, --cuprins
Introduceți un cuprins. Pentru o ieșire LATEX, inserează un \tableofcontents la
începutul documentului. Pentru o ieșire HTML, acesta creează un cuprins
în toc.html.

hiperlinkuri Opțiuni
--glob-de la fişier
Faceți referințe folosind globalizări Coq din fișierul fișier. (Asemenea globalizări sunt
obtinut cu optiunea Coq -dump-glob).

--fără-externe
Nu introduceți linkuri către biblioteca standard Coq.

--extern url libroot
Setați adresa URL de bază pentru biblioteca externă al cărei prefix rădăcină este libroot.

--coqlib url
Setați adresa URL de bază pentru biblioteca standard Coq (implicit este
http://coq.inria.fr/library/).

--coqlib_path dir
Setați calea de bază în care sunt instalate fișierele Coq, în special fișierele de stil
coqdoc.sty și coqdoc.css.

-R dir coqdir
Mapează directorul fizic directorul la directorul logic Coq coqdir (în mod similar cu opțiunea Coq
-R). Notă: opțiunea -R are efect numai asupra fișierelor care o urmează pe comandă
linie, deci probabil va trebui să puneți această opțiune pe primul loc.

Cuprins Opțiuni
-g, --gallina
Nu tipăriți dovezi.

-l, --ușoară
Modul de lumină. Suprimați dovezile (ca și cu -g) și următoarele comenzi:

* [Recursiv] Definiție tactică
* Sugestie / Sugestii
* Necesită
* Transparent / Opac
* Argument implicit / Implicit
* Sectiune / Variabila / Ipoteza / Sfarsit

Comportamentul opțiunilor -g și -l poate fi suprascris local folosind (* begin show
*) ... (* final show *) mediu (vezi mai sus).

Limbă Opțiuni
Comportamentul implicit este de a presupune fișiere de intrare ASCII de 7 biți.

-latină1, --latină1
Selectați fișierele de intrare ISO-8859-1. Este echivalent cu --inputenc latin1 --charset
izo-8859-1.

-utf8, --utf8
Selectați fișierele de intrare UTF-8 (Unicode). Este echivalent cu --inputenc utf8 --charset
utf-8. Suportul LATEX UTF-8 poate fi găsit la
http://www.ctan.org/tex-archive/macros/latex/contrib/supported/unicode/.

--inputenc şir
Dați o codificare de intrare LATEX, ca opțiune pentru pachetul LATEX inputenc.

--charset şir
Specificați setul de caractere HTML, care urmează să fie inserat în antetul HTML.

Utilizați coqdoc online folosind serviciile onworks.net