coqdoc - ອອນລາຍໃນຄລາວ

ໂຄງການ:

NAME

coqdoc - ເຄື່ອງມືເອກະສານສໍາລັບຜູ້ຊ່ວຍຫຼັກຖານສະແດງ Coq

ສະຫຼຸບສັງລວມ

coqdoc [ ທາງເລືອກໃນການ ] ໄຟ

ລາຍລະອຽດ

coqdoc ເປັນເຄື່ອງມືເອກະສານສໍາລັບຜູ້ຊ່ວຍຫຼັກຖານສະແດງ Coq. ມັນສ້າງ LaTeX ຫຼື HTML
ເອກະສານຈາກຊຸດຂອງໄຟລ໌ Coq. ເບິ່ງຄູ່ມືການອ້າງອີງ Coq ສໍາລັບເອກະສານ (url
ດ້ານລຸ່ມ).

OPTIONS

ໂດຍລວມ ທາງເລືອກໃນການ
-h ຊ່ວຍເຫຼືອ. ຈະໃຫ້ທ່ານບັນຊີລາຍຊື່ຄົບຖ້ວນຂອງທາງເລືອກທີ່ຍອມຮັບໂດຍ coqdoc.

--html ເລືອກຜົນຜະລິດ HTML.

-- ຢາງ
ເລືອກຜົນຜະລິດ LATEX.

--dvi ເລືອກຜົນຜະລິດ DVI.

--ps ເລືອກຜົນຜະລິດ PostScript.

--texmacs
ເລືອກຜົນຜະລິດ TeXmacs.

--stdout
ປ່ຽນເສັ້ນທາງຜົນຜະລິດໄປຫາ stdout

-o ແຟ້ມ,-- ຜົນຜະລິດ ເອກະສານ
ປ່ຽນເສັ້ນທາງຜົນຜະລິດເຂົ້າໄປໃນໄຟລ໌ ຍື່ນ.

-d ແມ່ນ, -- ບັນຊີລາຍການ dir
ໄຟລ​໌​ອອກ​ໄປ​ໃນ​ລະ​ບົບ​ dir ແທນທີ່ຈະເປັນໄດເລກະທໍລີປະຈຸບັນ (ທາງເລືອກ -d ບໍ່
ປ່ຽນຊື່ໄຟລ໌ທີ່ລະບຸດ້ວຍທາງເລືອກ -o, ຖ້າມີ).

- ແມ່ນແລ້ວ, --ສັ້ນ
ຢ່າໃສ່ຫົວຂໍ້ສໍາລັບໄຟລ໌. ພຶດຕິກໍາເລີ່ມຕົ້ນແມ່ນການໃສ່ຊື່ເຊັ່ນ
``ຫ້ອງສະໝຸດ Foo'' ສໍາລັບແຕ່ລະໄຟລ໌.

-t ສາຍ, --ຫົວຂໍ້ string
ຕັ້ງຊື່ເອກະສານ.

-- ຮ່າງກາຍເທົ່ານັ້ນ
ສະກັດກັ້ນສ່ວນຫົວ ແລະຕົວຢ່າງຂອງເອກະສານສຸດທ້າຍ. ດັ່ງນັ້ນ, ທ່ານສາມາດໃສ່
ເອກະສານຜົນໄດ້ຮັບເຂົ້າໄປໃນຂະຫນາດໃຫຍ່.

-p ສາຍ, -- ຄໍາບັນຍາຍ string
ໃສ່ບາງເອກະສານໃນ LATEX preamble, ກ່ອນ \begin{document}
(ບໍ່ມີຄວາມຫມາຍກັບ -html).

--vernac-file ແຟ້ມ, --tex-file ເອກະສານ
ພິຈາລະນາໄຟລ໌ 'ໄຟລ໌' ຕາມລໍາດັບເປັນໄຟລ໌ .v (ຫຼື .g) ຫຼືໄຟລ໌ .tex.

--files-ຈາກ ເອກະສານ
ອ່ານຊື່ໄຟລ໌ເພື່ອປະມວນຜົນໃນໄຟລ໌ 'ໄຟລ໌' ຄືກັບວ່າພວກເຂົາຖືກມອບໃຫ້ຢູ່ໃນຄໍາສັ່ງ
ສາຍ. ເປັນປະໂຫຍດສໍາລັບແຫຼ່ງໂຄງການແບ່ງອອກເປັນຫຼາຍໄດເລກະທໍລີ.

-q, --ງຽບ
ງຽບ. ຢ່າພິມຫຍັງຍົກເວັ້ນຂໍ້ຜິດພາດ.

-ຊ, - ຊ່ວຍ
ໃຫ້ສະຫຼຸບສັ້ນໆກ່ຽວກັບທາງເລືອກແລະອອກ.

- ໃນ​, - ການປ່ຽນແປງ
ພິມສະບັບແລະອອກ.

ດັດຊະນີ ທາງເລືອກໃນການ
ພຶດຕິກໍາເລີ່ມຕົ້ນແມ່ນການສ້າງດັດສະນີ, ສໍາລັບຜົນຜະລິດ HTML ເທົ່ານັ້ນ, ເຂົ້າໄປໃນ index.html.

--no-index
ບໍ່ໃຫ້ອອກດັດຊະນີ.

--multi-index
ສ້າງຫນ້າຫນຶ່ງສໍາລັບແຕ່ລະປະເພດແລະແຕ່ລະຕົວອັກສອນໃນດັດຊະນີ, ພ້ອມກັບ a
ຫນ້າເທິງ index.html.

ຕາຕະລາງ of ເນື້ອຫາ ທາງເລືອກ
-toc​, --ສາ​ລະ​ບານ
ໃສ່ຕາຕະລາງເນື້ອໃນ. ສໍາລັບຜົນຜະລິດ LATEX, ມັນແຊກ \tableofcontents ຢູ່
ຈຸດເລີ່ມຕົ້ນຂອງເອກະສານ. ສໍາລັບຜົນຜະລິດ HTML, ມັນສ້າງຕາຕະລາງເນື້ອໃນ
ເຂົ້າໄປໃນ toc.html.

hyperlinks ທາງເລືອກໃນການ
--glob-ຈາກ ເອກະສານ
ເຮັດການອ້າງອີງໂດຍໃຊ້ Coq globalizations ຈາກໄຟລ໌ໄຟລ໌. (ໂລກາພິວັດດັ່ງກ່າວແມ່ນ
ໄດ້ຮັບດ້ວຍທາງເລືອກ Coq -dump-glob).

-- ບໍ່​ມີ​ພາຍ​ນອກ​
ຢ່າໃສ່ລິ້ງໄປຫາຫ້ອງສະໝຸດມາດຕະຖານ Coq.

--ພາຍນອກ url libroot
ກໍານົດ URL ພື້ນຖານສໍາລັບຫ້ອງສະຫມຸດພາຍນອກທີ່ມີຄໍານໍາຫນ້າຮາກແມ່ນ libroot.

--coqlib url
ກໍານົດ URL ພື້ນຖານສໍາລັບຫ້ອງສະຫມຸດມາດຕະຖານ Coq (ຄ່າເລີ່ມຕົ້ນແມ່ນ
http://coq.inria.fr/library/).

--coqlib_path dir
ກໍານົດເສັ້ນທາງພື້ນຖານທີ່ໄຟລ໌ Coq ຖືກຕິດຕັ້ງ, ໂດຍສະເພາະໄຟລ໌ຮູບແບບ
coqdoc.sty ແລະ coqdoc.css.

-R dir coqdir
ແຜນທີ່ໄດເລກະທໍລີທາງດ້ານຮ່າງກາຍ dir ກັບ Coq ໄດເລກະທໍລີຢ່າງມີເຫດຜົນ coqdir (ຄ້າຍຄືກັນກັບທາງເລືອກ Coq
-R). ຫມາຍ​ເຫດ​: ທາງເລືອກ -R ພຽງແຕ່ມີຜົນກະທົບກັບໄຟລ໌ທີ່ປະຕິບັດຕາມມັນຢູ່ໃນຄໍາສັ່ງ
ເສັ້ນ, ດັ່ງນັ້ນທ່ານອາດຈະຈໍາເປັນຕ້ອງໃສ່ທາງເລືອກນີ້ກ່ອນ.

ເນື້ອໃນ ທາງເລືອກໃນການ
-g, -- ກາລີນາ
ຫ້າມພິມຫຼັກຖານ.

-l, --ແສງ
ໂໝດແສງ. ສະກັດກັ້ນຫຼັກຖານ (ເຊັ່ນດຽວກັບ -g) ແລະຄໍາສັ່ງຕໍ່ໄປນີ້:

* [Recursive] Tactic ຄໍານິຍາມ
* ຄໍາ​ແນະ​ນໍາ / ຄໍາ​ແນະ​ນໍາ​
* ຕ້ອງການ
* ໂປ່ງໃສ / opaque
* ການໂຕ້ຖຽງ implicit / implicits
* ພາກ/ຕົວແປ/ສົມມຸດຕິຖານ/ຈົບ

ພຶດຕິກໍາຂອງທາງເລືອກ -g ແລະ -l ສາມາດ overridden ໃນທ້ອງຖິ່ນໂດຍໃຊ້ (* start show
*) ... (* end show *) ສະພາບແວດລ້ອມ (ເບິ່ງຂ້າງເທິງ).

ພາສາ ທາງເລືອກໃນການ
ພຶດຕິກຳເລີ່ມຕົ້ນແມ່ນຖືວ່າ ASCII 7 bits input files.

- ລາ​ຕິນ 1​, --ລາຕິນ1
ເລືອກໄຟລ໌ປ້ອນຂໍ້ມູນ ISO-8859-1. ມັນເທົ່າກັບ --inputenc latin1 --charset
iso-8859-1.

-utf8, --utf8
ເລືອກໄຟລ໌ປ້ອນຂໍ້ມູນ UTF-8 (Unicode). ມັນເທົ່າກັບ --inputenc utf8 --charset
utf-8. ສະຫນັບສະຫນູນ LATEX UTF-8 ສາມາດພົບໄດ້ທີ່
http://www.ctan.org/tex-archive/macros/latex/contrib/supported/unicode/.

--ການປ້ອນຂໍ້ມູນ string
ໃຫ້ການເຂົ້າລະຫັດການປ້ອນຂໍ້ມູນ LATEX, ເປັນທາງເລືອກໃນການປ້ອນຂໍ້ມູນແພັກເກັດ LATEX.

--ຊຸດຕົວອັກສອນ string
ລະບຸຊຸດຕົວອັກສອນ HTML, ເພື່ອໃສ່ໃນສ່ວນຫົວ HTML.

ໃຊ້ coqdoc ອອນໄລນ໌ໂດຍໃຊ້ບໍລິການ onworks.net