هذا هو الأمر coqchk.opt الذي يمكن تشغيله في مزود الاستضافة المجانية OnWorks باستخدام إحدى محطات العمل المجانية المتعددة على الإنترنت مثل Ubuntu Online أو Fedora Online أو محاكي Windows عبر الإنترنت أو محاكي MAC OS عبر الإنترنت
برنامج:
اسم
coqchk - مدقق المكتبات المترجمة Coq Proof Checker
موجز
كوكتشك [ الخيارات ] نماذج
الوصف
كوكتشك هو المدقق المستقل للمكتبات المترجمة (ملفات .vo التي تنتجها coqc) لـ
مساعد إثبات Coq. راجع الدليل المرجعي لمزيد من المعلومات. يعود مع
الخروج من رمز 0 إذا نجحت جميع المهام المطلوبة. رمز الإرجاع غير الصفري يعني ذلك
حدث خطأ ما: لم يتم العثور على مكتبة ما ، محتوى تالف ، فحص النوع
الفشل ، إلخ.
نماذج هي قائمة الوحدات التي يجب التحقق منها. يمكن الإشارة إلى الوحدات النمطية باختصار أو
اسم مؤهل.
OPTIONS
-I دير --يشمل دير
إضافة دليل دير في مسار التضمين
-R دير com.coqdir
بشكل متكرر خريطة المادية دير لمنطقي com.coqdir
-صامتة
يجعل Coqchk أقل إطالة.
-يعترف وحدة
ضع علامة على الوحدة المحددة وجميع تبعياتها على أنها موثوقة ، ولن تكون كذلك
إعادة فحصها ، ما لم تطلبها خيارات أخرى صراحة.
-نوريك وحدة
يحدد أنه يجب التحقق من الوحدة النمطية المحددة دون طلب التحقق منها
التبعيات.
م ، --ذاكرة
يعرض ملخصًا للذاكرة المستخدمة بواسطة المدقق.
-o ، - سياق الإخراج
يعرض ملخصًا للمحتوى المنطقي الذي تم التحقق منه: الافتراضات و
استخدام اللامبالاة.
-مجموعة وصفية
يسمح للمدقق بقبول المكتبات التي تم تجميعها باستخدام هذه العلامة.
-v طباعة نسخة coqchk والخروج.
-ققلب دير
يتجاوز الموقع الافتراضي للمكتبة القياسية.
-أين طباعة موقع مكتبة coqchk القياسية والخروج.
-ح ، --مساعدة
طباعة قائمة الخيارات
استخدم coqchk.opt عبر الإنترنت باستخدام خدمات onworks.net
