| COQ-TEX(1) | General Commands Manual | COQ-TEX(1) |
نام (NAME)
coq-tex - پردازش عبارت‌های Coq تعبیه‌شده در فایل‌های LaTeX
خلاصه دستور (SYNOPSIS)
coq-tex [ -o output-file ] [ -n line-width ] [ -image coq-image ] [ -w ] [ -v ] [ -sl ] [ -hrule ] [ -small ] input-file ...
توضیحات (DESCRIPTION)
فیلتر coq-tex عبارت‌های Coq تعبیه‌شده در فایل‌های LaTeX را استخراج و ارزیابی کرده و نتیجهٔ ارزیابی را پس از هر عبارت درج می‌کند.
سه محیط LaTeX برای گنجاندن کد Coq در فایل‌های ورودی فراهم شده است:
- coq_example
- عبارت‌های میان \begin{coq_example} و \end{coq_example} ارزیابی شده و در فایل خروجی کپی می‌شوند. به دنبال هر عبارت، پاسخ حلقهٔ سطح‌بالا (toplevel loop) درج می‌شود.
- coq_example*
- عبارت‌های میان \begin{coq_example*} و \end{coq_example*} ارزیابی شده و در فایل خروجی کپی می‌شوند. پاسخ‌های حلقهٔ سطح‌بالا نادیده گرفته می‌شوند.
- coq_eval
- عبارت‌های میان \begin{coq_eval} و \end{coq_eval} به صورت خاموش ارزیابی می‌شوند. آن‌ها در فایل خروجی کپی نمی‌شوند و پاسخ‌های حلقهٔ سطح‌بالا نادیده گرفته می‌شوند.
کد LaTeX حاصل در فایل file.v.tex ذخیره می‌شود، در صورتی که نام فایل ورودی به شکل file.tex باشد؛ در غیر این صورت نام فایل خروجی همان نام فایل ورودی به همراه پسوند `.v.tex' خواهد بود.
فایل‌های تولیدشده توسط coq-tex می‌توانند مستقیماً توسط LaTeX پردازش شوند. هم عبارت‌های Coq و هم خروجی حلقهٔ سطح‌بالا با قلم ماشین‌تحریری (typewriter font) حروف‌چینی می‌شوند.
گزینه‌ها (OPTIONS)
- -o output-file
- نام فایلی را مشخص می‌کند که خروجی LaTeX باید در آن ذخیره شود. یک خط تیره `-' موجب چاپ خروجی LaTeX در خروجی استاندارد می‌شود.
- -n line-width
- عرض خط را تعیین می‌کند. مقدار پیش‌فرض ۷۲ نویسه است. اگر پاسخ‌های حلقهٔ سطح‌بالا طولانی‌تر از عرض خط باشند، شکسته می‌شوند. هیچ شکستی روی متن ورودی Coq اعمال نمی‌شود.
- -image coq-image
- باعث می‌شود فایل coq-image برای ارزیابی عبارت‌های Coq اجرا شود. به طور پیش‌فرض، از دستور coqtop بدون تعیین هیچ مسیری برای ارزیابی عبارت‌های Coq استفاده می‌شود.
- -w
- باعث می‌شود خطوط در صورت امکان روی نویسهٔ فاصله شکسته شوند تا از نصف شدن کلمات در خروجی جلوگیری گردد. به طور پیش‌فرض، شکستن خطوط بدون توجه به نصف شدن کلمات و در محدودهٔ عرض خط انجام می‌پذیرد.
- -v
- حالت پرگو (verbose). پاسخ‌های Coq را در خروجی استاندارد چاپ می‌کند. برای تشخیص خطاها در عبارت‌های Coq سودمند است.
- -sl
- حالت مایل (slanted). پاسخ‌های Coq با قلم مایل نوشته می‌شوند.
- -hrule
- حالت خطوط افقی. بخش‌های Coq میان دو خط افقی نوشته می‌شوند.
- -small
- حالت قلم کوچک. بخش‌های Coq با قلمی کوچک‌تر نوشته می‌شوند.
هشدارها (CAVEATS)
عبارت‌های \begin... و \end... باید به تنهایی در یک خط قرار گیرند، بدون هیچ نویسه‌ای پیش از بک‌اسلش یا پس از آکولاد بسته. هر عبارت Coq باید با یک `.' در انتهای خط خاتمه یابد. وجود فاصلهٔ خالی میان `.' و خط جدید مجاز است، اما هر نویسهٔ دیگر باعث می‌شود که coq-tex پایان عبارت را نادیده بگیرد، که این امر به درهم‌ریختگی و عدم تطابق پاسخ‌ها با عبارت‌ها می‌انجامد. (پاسخ‌ها «عقب می‌افتند».)