هذا هو الأمر coqtop الذي يمكن تشغيله في مزود الاستضافة المجانية OnWorks باستخدام إحدى محطات العمل المجانية المتعددة عبر الإنترنت مثل Ubuntu Online أو Fedora Online أو محاكي Windows عبر الإنترنت أو محاكي MAC OS عبر الإنترنت
برنامج:
اسم
coqtop - نظام المستوى العلوي المساعد Coq Proof Assistant
موجز
com.coqtop [ الخيارات ]
الوصف
com.coqtop هو نظام المستوى الأعلى من Coq ، للاستخدام التفاعلي. يقرأ العبارات على
الإدخال القياسي ، وطباعة النتائج على الإخراج القياسي.
لاستخدام Coq الموجه نحو الدُفعات ، انظر com.coqc(1).
OPTIONS
-ح ، --مساعدة
يساعد. سوف نقدم لك قائمة كاملة من الخيارات المقبولة من قبل coqtop.
-I دير --يشمل دير
إضافة دليل دير في مسار التضمين
-R دير com.coqdir
بشكل متكرر خريطة المادية دير لمنطقي com.coqdir
-أعلى com.coqdir
تعيين اسم المستوى ليكون com.coqdir بدلا من الأعلى
- دولة اسم الملف، -يكون اسم الملف
قراءة الحالة من الملف اسم الملف
-نويس تبدأ بحالة ابتدائية فارغة
-الدولةاسم الملف
كتابة الدولة في الملف اسم الملف
-حمل- مل- كائن اسم الملف
تحميل ملف كائن ML اسم الملف
-الحمل- مل- المصدر اسم الملف
تحميل ملف ML اسم الملف
-الحمولة-المصدر-اللغة الفرنسية اسم الملف، -l اسم الملف
تحميل ملف Coq اسم الملف (تحميل اسم الملف.)
-حمل-لغة-لغة-مصدر- مطوّل اسم الملف، -lv اسم الملف
تحميل ملف Coq مطولاً اسم الملف (تحميل اسم ملف مطول.)
-حمل-لغة-لغة-كائن اسم الملف
تحميل ملف كائن Coq اسم الملف.vo
-يتطلب اسم الملف
تحميل ملف كائن Coq اسم الملف.vo واستيراده (يتطلب استيراد اسم الملف.)
-جمع اسم الملف
تجميع ملف Coq اسم الملف (يدل -حزمة )
- تجميع مطول اسم الملف
ترجمة شفهية لملف Coq اسم الملف (يدل -حزمة )
-يختار، يقرر قم بتشغيل إصدار الكود الأصلي من Coq
بايت قم بتشغيل إصدار الرمز الثانوي من Coq
-أين طباعة موقع مكتبة Coq القياسي والخروج
-v طباعة نسخة Coq والخروج
-q تخطي تحميل rcfile
-init- ملف اسم الملف
تعيين rcfile إلى اسم الملف
-حزمة وضع الدُفعات (يخرج بعد تحليل الوسائط مباشرةً)
-حذاء طويل وضع التمهيد (يعني -q و -حزمة )
-أيماكس يخبر Coq أنه يتم تنفيذه تحت Emacs
تفريغ الكرة الأرضية اسم الملف
تفريغ عمليات العولمة في الملف f (ليتم استخدامها بواسطة كوكدوك(1) )
-مع-جيوبروف (نعم | لا)
إلى (إلغاء) تنشيط الوظائف الخاصة لـ Geoproof داخل Coqide (الافتراضي هو نعم فعلا )
-مجموعة وصفية
تعيين الفرز تعيين إلزامي
البراهين -لا تحميل-
لا تقم بتحميل البراهين غير الشفافة في الذاكرة
-xml تصدير ملفات XML إما إلى التسلسل الهرمي المتجذر في الدليل
$ COQ_XML_LIBRARY_ROOT $ (إذا تم التعيين) أو stdout (إذا لم يتم ضبطه)
الجودة
تحسين وضوح شروط الإثبات التي تنتجها بعض التكتيكات
استخدم coqtop عبر الإنترنت باستخدام خدمات onworks.net