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