نام (NAME)

coqdoc - ابزار مستندسازی برای دستیار اثبات Coq

خلاصه دستور (SYNOPSIS)

coqdoc [ گزینه‌ها ] فایل‌ها

توضیحات (DESCRIPTION)

coqdoc یک ابزار مستندسازی برای دستیار اثبات Coq است. این ابزار از مجموعه‌ای از فایل‌های Coq اسناد LaTeX یا HTML ایجاد می‌کند. برای مستندات به کتابچه راهنمای مرجع Coq مراجعه کنید (پیوند در زیر آمده است).

گزینه‌ها (OPTIONS)

گزینه‌های کلی

-h: راهنما. فهرست کاملی از گزینه‌های پذیرفته شده توسط coqdoc را ارائه می‌دهد.
--html: خروجی HTML را انتخاب می‌کند.
--latex: خروجی LaTeX را انتخاب می‌کند.
--dvi: خروجی DVI را انتخاب می‌کند.
--ps: خروجی PostScript را انتخاب می‌کند.
--texmacs: خروجی TeXmacs را انتخاب می‌کند.
--stdout: خروجی را به خروجی استاندارد (stdout) هدایت می‌کند.
-o file,--output file: خروجی را به فایل file هدایت می‌کند.
-d dir, --directory dir: فایل‌ها را به جای دایرکتوری جاری در دایرکتوری dir خروجی می‌دهد (گزینه -d نام فایل مشخص‌شده توسط گزینه -o را در صورت وجود، تغییر نمی‌دهد).
-s, --short: از درج عنوان برای فایل‌ها خودداری می‌کند. رفتار پیش‌فرض درج عنوانی مانند “Library Foo” برای هر فایل است.
-t string, --title string: عنوان سند را تنظیم می‌کند.
--body-only: سرایند و ته‌آیند سند نهایی را حذف می‌کند. بنابراین می‌توانید سند به‌دست‌آمده را درون یک سند بزرگ‌تر درج کنید.
-p string, --preamble string: مواردی را درست پیش از \begin{document} به پیش‌درآمد (preamble) سند LaTeX اضافه می‌کند (با -html بی‌معنی است).
--vernac-file file, --tex-file file: فایل file را به ترتیب به عنوان یک فایل .v (یا .g) یا یک فایل .tex در نظر می‌گیرد.
--files-from file: نام فایل‌ها برای پردازش را از فایل file می‌خواند، گویی که در خط فرمان داده شده‌اند. این گزینه برای کدهای منبع برنامه‌ای که در چند دایرکتوری تقسیم شده‌اند مفید است.
-q, --quiet: حالت ساکت. به جز خطاها چیزی چاپ نمی‌کند.
-h, --help: خلاصه‌ای کوتاه از گزینه‌ها را ارائه کرده و خارج می‌شود.
-v, --version: نسخه را چاپ کرده و خارج می‌شود.

گزینه‌های نمایه

رفتار پیش‌فرض، ساخت یک نمایه (تنها برای خروجی HTML) در فایل index.html است.

--no-index: نمایه را در خروجی تولید نمی‌کند.
--multi-index: برای هر دسته‌بندی و هر حرف در نمایه یک صفحه، به همراه یک صفحه اصلی به نام index.html تولید می‌کند.

گزینه فهرست مطالب

-toc, --table-of-contents: یک فهرست مطالب درج می‌کند. برای خروجی LaTeX، یک \tableofcontents در ابتدای سند درج می‌کند. برای خروجی HTML، یک فهرست مطالب در toc.html می‌سازد.

گزینه‌های پیوندها

--glob-from file: ارجاعات را با استفاده از سراسری‌سازی‌های Coq از فایل file ایجاد می‌کند. (چنین سراسری‌سازی‌هایی با گزینه Coq یعنی -dump-glob به دست می‌آیند).
--no-externals: پیوندهایی به کتابخانه استاندارد Coq درج نمی‌کند.
--external url libroot: نشانی اینترنتی (URL) پایه را برای کتابخانه خارجی که پیشوند ریشه آن libroot است تنظیم می‌کند.
--coqlib_url url: نشانی اینترنتی (URL) پایه را برای کتابخانه استاندارد Coq تنظیم می‌کند (پیش‌فرض http://coq.inria.fr/library است).
--coqlib dir: مسیر پایه‌ای را که فایل‌های Coq در آن نصب شده‌اند، به ویژه فایل‌های شیوه coqdoc.sty و coqdoc.css، مشخص می‌کند.
-R dir coqdir: دایرکتوری فیزیکی dir را به دایرکتوری منطقی Coq با نام coqdir نگاشت می‌کند (مشابه گزینه -R در Coq). نکته: گزینه -R تنها بر روی فایل‌هایی تأثیر می‌گذارد که پس از آن در خط فرمان قرار گرفته‌اند، بنابراین احتمالاً باید این گزینه را پیش از سایر گزینه‌ها قرار دهید.

گزینه‌های محتوا

-g, --gallina: اثبات‌ها را چاپ نمی‌کند.
-l, --light: حالت سبک (Light). اثبات‌ها (مانند -g) و دستورهای زیر را حذف می‌کند:

[Recursive] Tactic Definition
Hint / Hints
Require
Transparent / Opaque
Implicit Argument / Implicits
Section / Variable / Hypothesis / End

رفتار گزینه‌های -g و -l می‌تواند به صورت محلی با استفاده از محیط (* begin show *) ... (* end show *) بازنویسی شود (به بالا مراجعه کنید).

گزینه‌های زبان

رفتار پیش‌فرض، فرض کردن فایل‌های ورودی به عنوان اسکی (ASCII) ۷ بیتی است.

-latin1, --latin1: فایل‌های ورودی ISO-8859-1 را انتخاب می‌کند. این گزینه معادل است با --inputenc latin1 --charset iso-8859-1.
-utf8, --utf8: فایل‌های ورودی UTF-8 (یونیکد) را انتخاب می‌کند. این گزینه معادل است با --inputenc utf8 --charset utf-8. پشتیبانی LaTeX از UTF-8 را می‌توان در نشانی زیر یافت: http://www.ctan.org/tex-archive/macros/latex/contrib/supported/unicode
--inputenc string: یک کدگذاری ورودی LaTeX، به عنوان گزینه‌ای برای بسته inputenc در LaTeX، تعیین می‌کند.
--charset string: مجموعه نویسه‌های HTML را برای درج در سرایند HTML مشخص می‌کند.

همچنین ببینید (SEE ALSO)

The Rocq Prover Reference Manual.

وبگاه Rocq Prover: https://rocq-prover.org