coqdoc - Online sa Cloud

PROGRAMA:

NAME

coqdoc - Isang tool sa dokumentasyon para sa Coq proof assistant

SINOPSIS

coqdoc [ pagpipilian ] file

DESCRIPTION

coqdoc ay isang tool sa dokumentasyon para sa Coq proof assistant. Lumilikha ito ng LaTeX o HTML
mga dokumento mula sa isang hanay ng mga Coq file. Tingnan ang Coq reference manual para sa dokumentasyon (url
sa ibaba).

Opsyon

Pangkalahatang pagpipilian
-h Tulong. Ibibigay sa iyo ang kumpletong listahan ng mga opsyon na tinanggap ng coqdoc.

--html Pumili ng isang HTML na output.

--latex
Pumili ng LATEX na output.

--dvi Pumili ng isang DVI output.

--ps Pumili ng isang PostScript output.

--texmacs
Pumili ng output ng TeXmacs.

--stdout
I-redirect ang output sa stdout

-o file,--output file
I-redirect ang output sa file file.

-d ay, --direktoryo dir
Mag-output ng mga file sa direktoryo dir sa halip na kasalukuyang direktoryo (ang opsyon -d ay hindi
baguhin ang filename na tinukoy na may opsyon -o, kung mayroon man).

-oo, --maikli
Huwag magpasok ng mga pamagat para sa mga file. Ang default na pag-uugali ay ang pagpasok ng isang pamagat na tulad ng
``Library Foo'' para sa bawat file.

-t string, --pamagat pisi
Itakda ang pamagat ng dokumento.

--katawan-lamang
Pigilan ang header at trailer ng huling dokumento. Kaya, maaari mong ipasok ang
nagresultang dokumento sa isang mas malaki.

-p string, --preamble pisi
Maglagay ng ilang materyal sa LATEX preamble, bago ang \begin{document}
(walang kahulugan sa -html).

--vernac-file file, --tex-file file
Isinasaalang-alang ang file na `file' ayon sa pagkakabanggit bilang isang .v (o .g) na file o isang .tex na file.

--files-mula sa file
Basahin ang mga pangalan ng file upang iproseso sa file na `file' na parang ibinigay ang mga ito sa utos
linya. Kapaki-pakinabang para sa mga pinagmumulan ng programa na nahati sa ilang mga direktoryo.

-q, --tahimik
Manahimik ka. Huwag mag-print ng anuman maliban sa mga error.

-h, - Tumulong
Magbigay ng maikling buod ng mga opsyon at lumabas.

-sa, --bersyon
I-print ang bersyon at lumabas.

Index pagpipilian
Ang default na gawi ay ang bumuo ng isang index, para sa HTML na output lamang, sa index.html.

--walang-index
Huwag i-output ang index.

--multi-index
Bumuo ng isang pahina para sa bawat kategorya at bawat titik sa index, kasama ang a
tuktok na pahina index.html.

mesa of nilalaman opsyon
-toc, --talaan ng nilalaman
Maglagay ng talaan ng mga nilalaman. Para sa isang LATEX na output, naglalagay ito ng \tableofcontents sa
simula ng dokumento. Para sa isang HTML na output, ito ay bumubuo ng isang talaan ng mga nilalaman
sa toc.html.

Mga hyperlink pagpipilian
--glob-mula sa file
Gumawa ng mga sanggunian gamit ang mga globalisasyon ng Coq mula sa file file. (Ang ganitong mga globalisasyon ay
nakuha gamit ang opsyon ng Coq -dump-glob).

--walang mga panlabas
Huwag magpasok ng mga link sa Coq standard library.

--panlabas url libroot
Itakda ang base URL para sa external na library na ang root prefix ay libroot.

--coqlib url
Itakda ang base URL para sa Coq standard library (default ay
http://coq.inria.fr/library/).

--coqlib_path dir
Itakda ang base path kung saan naka-install ang mga Coq file, lalo na ang mga style file
coqdoc.sty at coqdoc.css.

-R dir coqdir
I-map ang physical directory dir sa Coq logical directory coqdir (katulad ng Coq option
-R). tandaan: Ang opsyon -R ay may epekto lamang sa mga file na sumusunod dito sa utos
linya, kaya malamang na kailangan mong ilagay muna ang opsyong ito.

Nilalaman pagpipilian
-g, --gallina
Huwag mag-print ng mga patunay.

-l, --liwanag
Light mode. Pigilan ang mga patunay (tulad ng sa -g) at ang mga sumusunod na utos:

* [Recursive] Tactic Definition
* Hint / Hint
* Mangangailangan
* Transparent / Opaque
* Implicit na Argumento / Implicits
* Seksyon / Variable / Hypothesis / Wakas

Ang pag-uugali ng mga opsyon -g at -l ay maaaring lokal na ma-override gamit ang (* begin show
*) ... (* end show *) environment (tingnan sa itaas).

Wika pagpipilian
Default na pag-uugali ay upang ipalagay ASCII 7 bits input file.

-latin1, --latin1
Piliin ang ISO-8859-1 input file. Ito ay katumbas ng --inputenc latin1 --charset
iso-8859-1.

-utf8, --utf8
Piliin ang UTF-8 (Unicode) input file. Ito ay katumbas ng --inputenc utf8 --charset
utf-8. Ang suporta sa LATEX UTF-8 ay matatagpuan sa
http://www.ctan.org/tex-archive/macros/latex/contrib/supported/unicode/.

--inputenc pisi
Magbigay ng LATEX input encoding, bilang opsyon sa LATEX package inputenc.

--charset pisi
Tukuyin ang HTML character set, na ilalagay sa HTML header.

Gamitin ang coqdoc online gamit ang mga serbisyo ng onworks.net