coqdoc - מקוון בענן

תָכְנִית:

שֵׁם

coqdoc - כלי תיעוד עבור עוזר הוכחת Coq

תַקצִיר

coqdoc [ אפשרויות ] קבצים

תיאור

coqdoc הוא כלי תיעוד עבור עוזר ההוכחה Coq. זה יוצר LaTeX או HTML
מסמכים מקבוצה של קבצי Coq. עיין במדריך העזר של Coq לתיעוד (כתובת אתר
להלן).

אפשרויות

באופן כללי אפשרויות
-h עֶזרָה. ייתן לך את הרשימה המלאה של האפשרויות המקובלות על ידי coqdoc.

--html בחר פלט HTML.

--שרף גומי
בחר פלט LATEX.

--dvi בחר פלט DVI.

--נ.ב בחר פלט PostScript.

--texmacs
בחר פלט TeXmacs.

--stdout
הפנה מחדש את הפלט ל-stdout

-o קובץ,--תְפוּקָה פילה
הפנה מחדש את הפלט לקובץ קובץ.

-d דיר, --מַדרִיך dir
פלט קבצים לתוך ספרייה dir במקום הספרייה הנוכחית (אפשרות -d לא
שנה את שם הקובץ שצוין עם אפשרות -o, אם יש).

-ס, --קצר
אל תכניס כותרות לקבצים. התנהגות ברירת המחדל היא הוספת כותרת כמו
``Library Foo'' עבור כל קובץ.

-t חוט, --כותרת מחרוזת
הגדר את כותרת המסמך.

--גוף בלבד
דחק את הכותרת והטריילר של המסמך הסופי. לפיכך, אתה יכול להכניס את
המסמך שהתקבל למסמך גדול יותר.

-p חוט, --הַקדָמָה מחרוזת
הכנס קצת חומר בהקדמה של LATEX, ממש לפני \begin{document}
(חסר משמעות עם -html).

---vernac-file קובץ, --tex-file פילה
מחשיב את הקובץ 'קובץ' בהתאמה כקובץ .v (או .g) או קובץ .tex.

--קבצים-מאת פילה
קרא את שמות הקבצים לעיבוד בקובץ `קובץ' כאילו הם ניתנו בפקודה
קַו. שימושי עבור מקורות תוכניות מפוצלים במספר ספריות.

-q, --שֶׁקֶט
תהיה בשקט. אל תדפיס שום דבר מלבד שגיאות.

-ח, - עזרה
תן סיכום קצר של האפשרויות וצא.

-ב, --גִרְסָה
הדפס את הגרסה וצא.

מדד אפשרויות
התנהגות ברירת המחדל היא לבנות אינדקס, עבור פלט HTML בלבד, לתוך index.html.

--ללא אינדקס
אל תוציא את האינדקס.

--מולטי אינדקס
צור עמוד אחד לכל קטגוריה ולכל אות באינדקס, יחד עם א
הדף העליון index.html.

טבלתי of תוכן אוֹפְּצִיָה
-טוק, --תוכן העניינים
הכנס תוכן עניינים. עבור פלט LATEX, הוא מוסיף \tableofcontents at
תחילת המסמך. עבור פלט HTML, הוא בונה תוכן עניינים
לתוך toc.html.

קישורים אפשרויות
--גלוב-מאת פילה
צור הפניות באמצעות גלובליזציות של Coq מקובץ קובץ. (גלובליזציות כאלה הן
מתקבל עם אפשרות Coq -dump-glob).

--ללא-חיצוניים
אל תכניס קישורים לספרייה הסטנדרטית של Coq.

--חיצוני כתובת אתר ליברוט
הגדר כתובת URL בסיסית עבור הספרייה החיצונית שקידומת הבסיס שלה היא libroot.

--coqlib כתובת אתר
הגדר כתובת URL בסיסית עבור הספרייה הסטנדרטית של Coq (ברירת המחדל היא
http://coq.inria.fr/library/).

--coqlib_path dir
הגדר את נתיב הבסיס שבו מותקנים קבצי Coq, במיוחד קבצי סגנון
coqdoc.sty ו-coqdoc.css.

-R dir coqdir
מפה את המדריך הפיזי ל-Coq הספרייה הלוגית coqdir (בדומה לאפשרות Coq
-ר). הערה: אפשרות -R משפיעה רק על הקבצים הבאים אחריה בפקודה
קו, אז כנראה שתצטרך לשים את האפשרות הזו קודם.

תוכן אפשרויות
-ג, --גלינה
אין להדפיס הגהות.

-ל, --אוֹר
מצב אור. דחק הוכחות (כמו ב-g) והפקודות הבאות:

* הגדרה טקטית [רקורסיבית]
* רמז / רמזים
* דורש
* שקוף / אטום
* טיעון משתמע / משתמע
* סעיף / משתנה / השערה / סוף

ניתן לעקוף את ההתנהגות של אפשרויות -g ו-l באופן מקומי באמצעות (* begin show
*) ... (* סוף מופע *) סביבה (ראה למעלה).

שפה אפשרויות
התנהגות ברירת המחדל היא להניח קבצי קלט ASCII 7 סיביות.

-לטינית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/.

--inputenc מחרוזת
תן קידוד קלט LATEX, כאופציה לחבילת LATEX inputenc.

--charset מחרוזת
ציין את ערכת התווים של HTML, שתתווסף בכותרת ה-HTML.

השתמש ב-coqdoc באינטרנט באמצעות שירותי onworks.net