coqdoc - ออนไลน์ในคลาวด์

โครงการ:

ชื่อ

coqdoc - เครื่องมือเอกสารสำหรับผู้ช่วยพิสูจน์ Coq

เรื่องย่อ

ค็อกด็อก [ ตัวเลือก ] ไฟล์

DESCRIPTION

ค็อกด็อก เป็นเครื่องมือเอกสารสำหรับผู้ช่วยพิสูจน์ Coq มันสร้าง LaTeX หรือ HTML
เอกสารจากชุดไฟล์ Coq ดูคู่มืออ้างอิง Coq สำหรับเอกสารประกอบ (url
ด้านล่าง)

OPTIONS

ทั้งหมด ตัวเลือก
-h ช่วย. จะแสดงรายการตัวเลือกทั้งหมดที่ coqdoc ยอมรับ

--html เลือกเอาต์พุต HTML

--ลาเท็กซ์
เลือกเอาต์พุต LATEX

--dvi เลือกเอาต์พุต DVI

--ปล เลือกเอาต์พุต PostScript

--เท็กซัส
เลือกเอาต์พุต TeXmacs

--stdout
เปลี่ยนเส้นทางเอาต์พุตไปที่ stdout

-o ไฟล์,--เอาท์พุท ไฟล์
เปลี่ยนเส้นทางเอาต์พุตไปยังไฟล์ ไฟล์

-d ผบ. --ไดเรกทอรี dir
ส่งออกไฟล์ไปยังไดเร็กทอรี dir แทนไดเร็กทอรีปัจจุบัน (ตัวเลือก -d ไม่
เปลี่ยนชื่อไฟล์ที่ระบุด้วยตัวเลือก -o ถ้ามี)

-NS, --สั้น
ห้ามใส่ชื่อไฟล์ พฤติกรรมเริ่มต้นคือการแทรกชื่อเช่น
``Library Foo'' สำหรับแต่ละไฟล์

-t สตริง --ชื่อ เชือก
ตั้งชื่อเอกสาร

--ตัวเท่านั้น
ระงับส่วนหัวและส่วนท้ายของเอกสารสุดท้าย ดังนั้น คุณสามารถแทรก
ส่งผลให้เอกสารมีขนาดใหญ่ขึ้น

-p สตริง --คำนำ เชือก
แทรกเนื้อหาบางส่วนในคำนำ LATEX ก่อน \begin{document}
(ไม่มีความหมายกับ -html)

--vernac-ไฟล์ ไฟล์, --เท็กซ์-ไฟล์ ไฟล์
พิจารณาไฟล์ `ไฟล์' ตามลำดับเป็นไฟล์ .v (หรือ .g) หรือไฟล์ .tex

--files-จาก ไฟล์
อ่านชื่อไฟล์ที่จะประมวลผลในไฟล์ `file' ราวกับว่าได้รับคำสั่ง
ไลน์. มีประโยชน์สำหรับแหล่งโปรแกรมที่แยกออกเป็นหลายไดเร็กทอรี

-NS, --เงียบ
เงียบไว้ ห้ามพิมพ์สิ่งใดนอกจากข้อผิดพลาด

-ชม, --ช่วยด้วย
ให้ข้อมูลสรุปสั้น ๆ ของตัวเลือกและออก

-ใน, --รุ่น
พิมพ์เวอร์ชันและออก

ดัชนี ตัวเลือก
พฤติกรรมเริ่มต้นคือการสร้างดัชนี สำหรับเอาต์พุต HTML เท่านั้น ลงใน index.html

--ไม่มีดัชนี
อย่าส่งออกดัชนี

--หลายดัชนี
สร้างหนึ่งหน้าสำหรับแต่ละหมวดหมู่และแต่ละตัวอักษรในดัชนีพร้อมกับ a
หน้าบนสุด index.html

ตาราง of เนื้อหา ตัวเลือก
-โทค, --สารบัญ
แทรกสารบัญ สำหรับเอาต์พุต LATEX จะแทรก \tableofcontents ที่
จุดเริ่มต้นของเอกสาร สำหรับเอาต์พุต HTML จะสร้างสารบัญ
ลงใน toc.html

เชื่อมโยงหลายมิติ ตัวเลือก
--glob-จาก ไฟล์
ทำการอ้างอิงโดยใช้ Coq globalizations จากไฟล์ (โลกาภิวัตน์ดังกล่าวคือ
ได้รับด้วยตัวเลือก Coq -dump-glob)

--ไม่มีภายนอก
อย่าแทรกลิงก์ไปยังไลบรารีมาตรฐาน Coq

--ภายนอก URL ลิบรูต
ตั้งค่า URL พื้นฐานสำหรับไลบรารีภายนอกที่มีคำนำหน้ารูทคือ libroot

--coqlib URL
ตั้งค่า URL พื้นฐานสำหรับไลบรารีมาตรฐาน Coq (ค่าเริ่มต้นคือ
http://coq.inria.fr/library/).

--coqlib_path dir
กำหนดพาธฐานที่ติดตั้งไฟล์ Coq โดยเฉพาะไฟล์สไตล์
coqdoc.sty และ coqdoc.css

-R dir ค็อกเดียร์
แม็พฟิสิคัลไดเร็กทอรี dir กับ Coq โลจิคัลไดเร็กทอรี coqdir (คล้ายกับ Coq option
-NS). หมายเหตุ ตัวเลือก -R มีผลเฉพาะกับไฟล์ที่ตามมาในคำสั่ง
ดังนั้นคุณอาจจะต้องใส่ตัวเลือกนี้ก่อน

เนื้อหา ตัวเลือก
-NS, --กัลลิน่า
ห้ามพิมพ์หลักฐาน

-l --แสงสว่าง
โหมดแสง ระงับการพิสูจน์ (เช่นเดียวกับ -g) และคำสั่งต่อไปนี้:

* [เรียกซ้ำ] นิยามยุทธวิธี
* คำแนะนำ / คำแนะนำ
* จำเป็นต้อง
* โปร่งใส / ทึบแสง
* อาร์กิวเมนต์โดยนัย / โดยนัย
* ส่วน / ตัวแปร / สมมติฐาน / สิ้นสุด

พฤติกรรมของตัวเลือก -g และ -l สามารถแทนที่ในเครื่องได้โดยใช้คำสั่ง (* start show
*) ... (* end show *) สภาพแวดล้อม (ดูด้านบน)

ภาษา ตัวเลือก
พฤติกรรมเริ่มต้นคือถือว่าไฟล์อินพุต ASCII 7 บิต

-latin1, --ละติน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/.

--อินพุต เชือก
ให้การเข้ารหัสอินพุต LATEX เป็นตัวเลือกสำหรับแพ็คเกจ LATEX inputenc

--ชุดอักขระ เชือก
ระบุชุดอักขระ HTML ที่จะแทรกในส่วนหัวของ HTML

ใช้ coqdoc ออนไลน์โดยใช้บริการ onworks.net