.TH COQDOC 1
.
.SH "نام (NAME)"
coqdoc \- ابزار مستندسازی برای دستیار اثبات Coq
.
.
.SH "خلاصه دستور (SYNOPSIS)"
.B coqdoc
[
گزینه‌ها
]
.I فایل‌ها
.
.
.SH "توضیحات (DESCRIPTION)"
.
.B coqdoc
یک ابزار مستندسازی برای دستیار اثبات Coq است.
این ابزار از مجموعه‌ای از فایل‌های Coq اسناد LaTeX یا HTML ایجاد می‌کند.
برای مستندات به کتابچه راهنمای مرجع Coq مراجعه کنید (پیوند در زیر آمده است).
.
.
.SH "گزینه‌ها (OPTIONS)"
.
.SS گزینه‌های کلی
.
.TP
.B \-h
راهنما.
فهرست کاملی از گزینه‌های پذیرفته شده توسط
.BR coqdoc
را ارائه می‌دهد.
.TP
.B \-\-html
خروجی HTML را انتخاب می‌کند.
.TP
.B \-\-latex
خروجی LaTeX را انتخاب می‌کند.
.TP
.B \-\-dvi
خروجی DVI را انتخاب می‌کند.
.TP
.B \-\-ps
خروجی PostScript را انتخاب می‌کند.
.TP
.B \-\-texmacs
خروجی TeXmacs را انتخاب می‌کند.
.TP
.B \-\-stdout
خروجی را به خروجی استاندارد (stdout) هدایت می‌کند.
.TP
.BI \-o \ file, \-\-output \ file
خروجی را به فایل
.I file
هدایت می‌کند.
.TP
.BI \-d \ dir, \ \-\-directory \ dir
فایل‌ها را به جای دایرکتوری جاری در دایرکتوری
.I dir
خروجی می‌دهد (گزینه
.B \-d
نام فایل مشخص‌شده توسط گزینه
.BR \-o
را در صورت وجود، تغییر نمی‌دهد).
.TP
.BR \-s , \ \-\-short
از درج عنوان برای فایل‌ها خودداری می‌کند.
رفتار پیش‌فرض درج عنوانی مانند \(lqLibrary Foo\(rq برای هر فایل است.
.TP
.BI \-t \ string, \ \-\-title \ string
عنوان سند را تنظیم می‌کند.
.TP
.B \-\-body\-only
سرایند و ته‌آیند سند نهایی را حذف می‌کند.
بنابراین می‌توانید سند به‌دست‌آمده را درون یک سند بزرگ‌تر درج کنید.
.TP
.BI \-p \ string, \ \-\-preamble \ string
مواردی را درست پیش از
\\begin{document}
به پیش‌درآمد (preamble) سند LaTeX اضافه می‌کند (با \-html بی‌معنی است).
.TP
.BI \-\-vernac\-file \ file, \ \-\-tex\-file \ file
فایل
.I file
را به ترتیب به عنوان یک فایل .v (یا .g) یا یک فایل .tex در نظر می‌گیرد.
.TP
.BI \-\-files\-from \ file
نام فایل‌ها برای پردازش را از فایل
.I file
می‌خواند، گویی که در خط فرمان داده شده‌اند.
این گزینه برای کدهای منبع برنامه‌ای که در چند دایرکتوری تقسیم شده‌اند مفید است.
.TP
.BR \-q , \ \-\-quiet
حالت ساکت.
به جز خطاها چیزی چاپ نمی‌کند.
.TP
.BR \-h , \ \-\-help
خلاصه‌ای کوتاه از گزینه‌ها را ارائه کرده و خارج می‌شود.
.TP
.BR \-v , \ \-\-version
نسخه را چاپ کرده و خارج می‌شود.
.
.SS گزینه‌های نمایه
.
رفتار پیش‌فرض، ساخت یک نمایه (تنها برای خروجی HTML) در فایل index.html است.
.
.TP
.B \-\-no\-index
نمایه را در خروجی تولید نمی‌کند.
.TP
.B \-\-multi\-index
برای هر دسته‌بندی و هر حرف در نمایه یک صفحه، به همراه یک صفحه اصلی به نام index.html تولید می‌کند.
.
.SS گزینه فهرست مطالب
.
.TP
.BR \-toc , \ \-\-table\-of\-contents
یک فهرست مطالب درج می‌کند.
برای خروجی LaTeX، یک \\tableofcontents در ابتدای سند درج می‌کند.
برای خروجی HTML، یک فهرست مطالب در toc.html می‌سازد.
.
.SS گزینه‌های پیوندها
.
.TP
.BI \-\-glob\-from \ file
ارجاعات را با استفاده از سراسری‌سازی‌های Coq از فایل file ایجاد می‌کند.
(چنین سراسری‌سازی‌هایی با گزینه Coq یعنی
.BR \-dump\-glob
به دست می‌آیند).
.
.TP
.B \-\-no\-externals
پیوندهایی به کتابخانه استاندارد Coq درج نمی‌کند.
.
.TP
.BI \-\-external \ url\ libroot
نشانی اینترنتی (URL) پایه را برای کتابخانه خارجی که پیشوند ریشه آن
.I libroot
است تنظیم می‌کند.
.
.TP
.BI \-\-coqlib_url \ url
نشانی اینترنتی (URL) پایه را برای کتابخانه استاندارد Coq تنظیم می‌کند (پیش‌فرض
http://coq.inria.fr/library
است).
.
.TP
.BI \-\-coqlib \ dir
مسیر پایه‌ای را که فایل‌های Coq در آن نصب شده‌اند، به ویژه فایل‌های شیوه coqdoc.sty و coqdoc.css، مشخص می‌کند.
.
.TP
.BI \-R \ dir\ coqdir
دایرکتوری فیزیکی dir را به دایرکتوری منطقی Coq با نام coqdir نگاشت می‌کند (مشابه گزینه
.BR \-R
در Coq).
.B نکته:
گزینه
.B \-R
تنها بر روی فایل‌هایی تأثیر می‌گذارد که پس از آن در خط فرمان قرار گرفته‌اند، بنابراین احتمالاً باید این گزینه را پیش از سایر گزینه‌ها قرار دهید.
.
.SS گزینه‌های محتوا
.
.TP
.BR \-g , \ \-\-gallina
اثبات‌ها را چاپ نمی‌کند.
.
.TP
.BR \-l , \ \-\-light
حالت سبک (Light). اثبات‌ها (مانند
.BR \-g )
و دستورهای زیر را حذف می‌کند:
.RS
.IP \(bu 3
[Recursive] Tactic Definition
.IP \(bu
Hint / Hints
.IP \(bu
Require
.IP \(bu
Transparent / Opaque
.IP \(bu
Implicit Argument / Implicits
.IP \(bu
Section / Variable / Hypothesis / End
.PP
رفتار گزینه‌های
.B \-g
و
.B \-l
می‌تواند به صورت محلی با استفاده از محیط (*\ begin show\ *) .\|.\|. (*\ end show\ *) بازنویسی شود (به بالا مراجعه کنید).
.RE
.
.SS گزینه‌های زبان
.
رفتار پیش‌فرض، فرض کردن فایل‌های ورودی به عنوان اسکی (ASCII) ۷ بیتی است.
.
.TP
.BR \-latin1 , \ \-\-latin1
فایل‌های ورودی ISO-8859-1 را انتخاب می‌کند.
این گزینه معادل است با
.BR "\-\-inputenc\ latin1 \-\-charset\ iso\-8859\-1" .
.
.TP
.BR \-utf8 , \ \-\-utf8
فایل‌های ورودی UTF-8 (یونیکد) را انتخاب می‌کند.
این گزینه معادل است با
.BR "\-\-inputenc\ utf8 \-\-charset\ utf\-8" .
پشتیبانی LaTeX از UTF-8 را می‌توان در نشانی زیر یافت:
http://www.ctan.org/tex\-archive/macros/latex/contrib/supported/unicode
.
.TP
.BI \-\-inputenc \ string
یک کدگذاری ورودی LaTeX، به عنوان گزینه‌ای برای بسته inputenc در LaTeX، تعیین می‌کند.
.
.TP
.BI \-\-charset \ string
مجموعه نویسه‌های HTML را برای درج در سرایند HTML مشخص می‌کند.
.
.
.SH "همچنین ببینید (SEE ALSO)"
.
.I
The Rocq Prover Reference Manual.
.PP
وبگاه Rocq Prover: https://rocq-prover.org