coqdoc - آنلاین در ابر

برنامه:

نام

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

خلاصه

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

شرح

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

OPTIONS

به طور کلی گزینه های
-h کمک. لیست کاملی از گزینه های پذیرفته شده توسط coqdoc را به شما می دهد.

--html یک خروجی HTML را انتخاب کنید.

--لاتکس
یک خروجی لاتکس را انتخاب کنید.

--dvi یک خروجی DVI را انتخاب کنید.

--ps یک خروجی PostScript را انتخاب کنید.

--texmacs
یک خروجی TeXmacs را انتخاب کنید.

--stdout
خروجی را به stdout تغییر مسیر دهید

-o فایل،-- خروجی پرونده
خروجی را به فایل هدایت کنید فایل.

-d dir ، --فهرست راهنما دیر
خروجی فایل ها در دایرکتوری دیر به جای دایرکتوری فعلی (گزینه -d ندارد
نام فایل مشخص شده را با گزینه -o در صورت وجود تغییر دهید).

-s ، --کوتاه
از درج عنوان برای فایل ها خودداری کنید. رفتار پیش فرض این است که عنوانی مانند درج کنید
"Library Foo" برای هر فایل.

-t رشته، --عنوان رشته
عنوان سند را تنظیم کنید.

--فقط برای بدن
سربرگ و تریلر سند نهایی را سرکوب کنید. بنابراین، شما می توانید وارد کنید
سند در نتیجه به یک سند بزرگتر تبدیل شود.

-p رشته، -- مقدمه رشته
مقداری مطالب را در مقدمه LATEX، درست قبل از \begin{document} وارد کنید
(بی معنی با -html).

--vernac-فایل فایل، --tex-file پرونده
فایل 'file' را به ترتیب به عنوان یک فایل .v (یا .g) یا یک فایل .tex در نظر می گیرد.

--فایلها-از پرونده
نام فایل‌ها را برای پردازش در فایل «فایل» بخوانید، به‌گونه‌ای که گویی در دستور داده شده‌اند
خط مفید برای منابع برنامه تقسیم شده در چندین فهرست.

-q، --ساکت
ساکت باش. جز خطاها چیزی چاپ نکنید.

-h، --کمک
یک خلاصه کوتاه از گزینه ها ارائه دهید و خارج شوید.

-v، - نسخه
نسخه را پرینت بگیرید و خارج شوید.

شاخص گزینه های
رفتار پیش‌فرض این است که یک فهرست، فقط برای خروجی HTML، در index.html بسازید.

--بدون شاخص
شاخص را خروجی ندهید.

--چند شاخص
یک صفحه برای هر دسته و هر حرف در فهرست به همراه a ایجاد کنید
صفحه بالا index.html.

جدول of محتویات انتخاب
-toc، --فهرست مطالب
فهرست مطالب را درج کنید. برای خروجی لاتکس، \tableofcontents را درج می کند
ابتدای سند برای خروجی HTML، فهرست مطالب را می سازد
به toc.html.

لینک گزینه های
--glob-از پرونده
با استفاده از جهانی سازی های Coq از فایل فایل، ارجاع دهید. (این گونه جهانی سازی ها هستند
به دست آمده با گزینه Coq -dump-glob).

-- بدون خارجی
پیوندهایی را به کتابخانه استاندارد Coq وارد نکنید.

-- خارجی آدرس لیبروت
URL پایه را برای کتابخانه خارجی که پیشوند ریشه آن libroot است تنظیم کنید.

-- coqlib آدرس
URL پایه را برای کتابخانه استاندارد Coq تنظیم کنید (پیش‌فرض است
http://coq.inria.fr/library/).

--coqlib_path دیر
مسیر پایه را که فایل‌های Coq نصب می‌شوند، مخصوصا فایل‌های سبک را تنظیم کنید
coqdoc.sty و coqdoc.css.

-R دیر coqdir
نقشه دایرکتوری فیزیکی dir به دایرکتوری منطقی Coq coqdir (همانند گزینه Coq
-R). توجه داشته باشید: گزینه -R فقط بر روی فایل های زیر در دستور اثر دارد
خط، بنابراین احتمالاً باید ابتدا این گزینه را قرار دهید.

فهرست گزینه های
-g، --گالینا
مدارک را چاپ نکنید.

-ل، --سبک
حالت نور. اثبات (مانند -g) و دستورات زیر را سرکوب کنید:

* [بازگردانی] تعریف تاکتیک
* نکته / نکات
* نیاز
* شفاف / مات
* استدلال ضمنی / ضمنی
* بخش / متغیر / فرضیه / پایان

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

زبان گزینه های
رفتار پیش فرض این است که فایل های ورودی ASCII 7 بیتی را فرض کنیم.

-لاتین1، --لاتین 1
فایل های ورودی 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 رشته
یک رمزگذاری ورودی LATEX به عنوان یک گزینه به بسته ورودی LATEX بدهید.

-- مجموعه حروف رشته
مجموعه کاراکترهای HTML را مشخص کنید تا در هدر HTML درج شود.

با استفاده از خدمات onworks.net از coqdoc به صورت آنلاین استفاده کنید