זוהי הפקודה coqchk.opt שניתן להפעיל בספק האירוח החינמי של OnWorks באמצעות אחת מתחנות העבודה המקוונות המרובות שלנו בחינם כגון Ubuntu Online, Fedora Online, אמולטור מקוון של Windows או אמולטור מקוון של MAC OS
תָכְנִית:
שֵׁם
coqchk - מאמת ספריות הידור של Coq Proof Checker
תַקצִיר
coqchk [ אפשרויות ] מודולים
תיאור
coqchk הוא הבודק העצמאי של ספריות הידור (קבצי.vo המיוצרים על ידי coqc) עבור
עוזר ההוכחה של Coq. עיין במדריך העזר למידע נוסף. זה חוזר עם
צא מקוד 0 אם כל המשימות המבוקשות הצליחו. קוד החזרה שאינו אפס אומר זאת
משהו השתבש: ספרייה כלשהי לא נמצאה, תוכן פגום, בדיקת סוגים
כישלון וכו'.
מודולים היא רשימה של מודולים שיש לבדוק. ניתן להתייחס למודולים באמצעות קצר או
שם מוסמך.
אפשרויות
-I דיר, --לִכלוֹל dir
הוסף ספרייה dir בנתיב הכלול
-R dir coqdir
ממפה פיזית רקורסיבית dir להגיוני coqdir
-שקט
עושה את coqchk פחות מילולי.
-להתוודות מודול
תייג את המודול שצוין ואת כל התלות שלו כאמין, ולא יהיה
נבדק מחדש, אלא אם כן התבקש מפורשות על ידי אפשרויות אחרות.
-נורק מודול
מציין שהמודול הנתון יאומת מבלי לבקש לבדוק אותו
תלות.
-M, --זיכרון
מציג סיכום של הזיכרון שבו משתמש הבודק.
-או, --הקשר פלט
מציג סיכום של התוכן ההגיוני שאומת: הנחות ו
שימוש באי-פרדיקטיביות.
-סט אימפריקטיבי
מאפשר לבודק לקבל ספריות שהורכבו עם דגל זה.
-v הדפס גרסת coqchk וצא.
-קוקליב dir
עוקף את מיקום ברירת המחדל של הספרייה הסטנדרטית.
-איפה הדפס מיקום ויציאה מהספרייה הסטנדרטית של coqchk.
-ח, - עזרה
להדפיס רשימה של אפשרויות
השתמש ב-coqchk.opt באינטרנט באמצעות שירותי onworks.net
