هذا هو الأمر coqdoc الذي يمكن تشغيله في مزود الاستضافة المجانية OnWorks باستخدام إحدى محطات العمل المجانية المتعددة على الإنترنت مثل Ubuntu Online أو Fedora Online أو محاكي Windows عبر الإنترنت أو محاكي MAC OS عبر الإنترنت
برنامج:
اسم
coqdoc - أداة توثيق لمساعد إثبات Coq
موجز
كوكدوك [ الخيارات ] ملفات
الوصف
كوكدوك هي أداة توثيق لمساعد إثبات Coq. يقوم بإنشاء LaTeX أو HTML
المستندات من مجموعة من ملفات Coq. راجع الدليل المرجعي Coq للتوثيق (url
أدناه).
OPTIONS
أوفرول الخيارات
-h يساعد. سوف نقدم لك قائمة كاملة من الخيارات المقبولة من قبل coqdoc.
--لغة البرمجة حدد ناتج HTML.
--لاتكس
حدد إخراج لاتكس.
--dvi حدد مخرج DVI.
--ملاحظة حدد إخراج PostScript.
--تكسماكس
حدد إخراج TeXmacs.
- stdout
إعادة توجيه الإخراج إلى stdout
-o ملف،--انتاج ملف
أعد توجيه الإخراج إلى الملف ملف.
-d دير --الدليل دير
إخراج الملفات إلى الدليل دير بدلا من الدليل الحالي (الخيار -d لا
قم بتغيير اسم الملف المحدد بالخيار -o ، إن وجد).
-س، --قصيرة
لا تقم بإدراج عناوين للملفات. السلوك الافتراضي هو إدراج عنوان مثل
`` Library Foo '' لكل ملف.
-t خيط، --لقب سلسلة
قم بتعيين عنوان المستند.
--الجسم فقط
قم بإلغاء العنوان والمقطورة الخاصة بالمستند النهائي. وبالتالي ، يمكنك إدخال ملف
الناتج إلى مستند أكبر.
-p خيط، - تصديق سلسلة
أدخل بعض المواد في مقدمة LATEX ، قبل \ start {document} مباشرةً
(لا معنى له مع html).
- ملف vernac ملف، --ملف تكس ملف
يعتبر الملف "ملف" على التوالي كملف .v (أو .g) أو ملف .tex.
- ملفات من ملف
اقرأ أسماء الملفات المراد معالجتها في ملف "ملف" كما لو تم تقديمها في الأمر
خط. مفيد لمصادر البرنامج المقسمة إلى عدة أدلة.
-q ، --هادئ
كن هادئاً. لا تطبع أي شيء باستثناء الأخطاء.
-ح ، --مساعدة
قدم ملخصًا موجزًا للخيارات والخروج.
-الخامس، --الإصدار
اطبع النسخة واخرج.
فهرس الخيارات
السلوك الافتراضي هو بناء فهرس ، لإخراج HTML فقط ، في index.html.
--لا يوجد فهرس
لا تخرج الفهرس.
- متعدد الفهرس
قم بإنشاء صفحة واحدة لكل فئة وكل حرف في الفهرس ، مع ملف
أعلى صفحة index.html.
طاولات ومكاتب of محتويات خيار
-Toc ، --جدول المحتويات
أدخل جدول محتويات. بالنسبة لمخرج LATEX ، فإنه يُدرج \ tableofcontents في
بداية المستند. بالنسبة لمخرج HTML ، فإنه ينشئ جدول محتويات
إلى toc.html.
الارتباطات التشعبية الخيارات
--جلوب من ملف
قم بعمل مراجع باستخدام عولمة Coq من ملف الملف. (مثل هذه العولمة
تم الحصول عليها باستخدام خيار Coq -dump-glob).
- لا خارجي
لا تقم بإدراج ارتباطات إلى مكتبة Coq القياسية.
--خارجي URL ليبروت
قم بتعيين عنوان URL الأساسي للمكتبة الخارجية التي تكون بادئة الجذر الخاصة بها هي libroot.
- كوكليب URL
قم بتعيين عنوان URL الأساسي لمكتبة Coq القياسية (الافتراضي هو
http://coq.inria.fr/library/).
--coqlib_path دير
قم بتعيين المسار الأساسي حيث يتم تثبيت ملفات Coq ، خاصة ملفات الأنماط
coqdoc.sty و coqdoc.css.
-R دير com.coqdir
قم بتعيين دليل الدليل المادي إلى دليل Coq المنطقي coqdir (على غرار خيار Coq
-ر). ملحوظة: الخيار -R له تأثير فقط على الملفات التي تتبعه في الأمر
لذلك ربما تحتاج إلى وضع هذا الخيار أولاً.
المحتويات الخيارات
-g ، - غالينا
لا تطبع البراهين.
-ل ، --ضوء
وضع الضوء. قم بإلغاء البراهين (كما هو الحال مع -g) والأوامر التالية:
* تعريف تكتيكي [تكراري]
* تلميحات / تلميحات
* يتطلب
* شفاف / معتم
* الحجج الضمنية / التضمينات
* قسم / متغير / فرضية / نهاية
يمكن تجاوز سلوك الخيارين -g و -l محليًا باستخدام (* start 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/.
- المدخلات سلسلة
أعط ترميز إدخال LATEX ، كخيار لإدخال حزمة LATEX.
- شارست سلسلة
حدد مجموعة أحرف HTML ، لإدراجها في رأس HTML.
استخدم coqdoc عبر الإنترنت باستخدام خدمات onworks.net
