זהו הפקודה coqide שניתן להפעיל בספק האירוח החינמי של OnWorks באמצעות אחת מתחנות העבודה המקוונות המרובות שלנו, כגון Ubuntu Online, Fedora Online, אמולטור מקוון של Windows או אמולטור מקוון של MAC OS
תָכְנִית:
שֵׁם
coqide - הממשק הגרפי של Coq Proof Assistant
תַקצִיר
קוקיד [ אפשרויות ]
תיאור
קוקיד הוא ממשק גרפי gtk עבור עוזר ההוכחה Coq.
לשימוש מונחה שורת פקודה ב-Coq, ראה coqtop(1); לשימוש מונחה אצווה ב-Coq, ראה
coqc(1).
אפשרויות
-h הצג את הרשימה המלאה של האפשרויות המקובלות על ידי קוקיד.
-I dir, -לִכלוֹל dir
הוסף directory dir בנתיב include.
-R dir coqdir
מפה פיזית רקורסיבית dir להגיוני coqdir.
-src הוסף ספריות מקור בנתיב הכללה.
-זה f, -מצב קלט f
קרא מצב מ f.coq.
-רעש התחל עם מצב ריק.
-מצב פלט f
כתוב מצב בקובץ f.coq.
-load-ml-object f
טען קובץ אובייקט ML f.
-load-ml-source f
טען קובץ ML f.
-l f, -load-vernac-source f
טען קובץ Coq f.v (טען f.).
-lv f, -load-vernac-source-verbose f
טען קובץ Coq f.v (טען מילולית f.).
-load-vernac-object f
טען קובץ אובייקט Coq f.vo.
-לִדרוֹשׁ f
טען קובץ אובייקט Coq f.vo וייבא אותו (דרוש f.).
-לְלַקֵט f
הידור קובץ Coq f.v (מרמז -קבוצה).
-compile-verbose f
קומפלור מילולי של קובץ Coq f.v (מרמז -קבוצה).
-העדיף הפעל את גרסת הקוד המקורי של Coq או Coq_SearchIsos.
-בייט הפעל את גרסת ה-bytecode של Coq או Coq_SearchIsos.
-איפה הדפס את מיקום הספרייה הסטנדרטי של Coq ויציאה.
-v הדפס את גרסת Coq וצא.
-q דלג על טעינת rcfile.
-init-file f
הגדר את rcfile ל f.
-קבוצה מצב אצווה (יוצא מיד לאחר ניתוח ארגומנטים).
-מַגָף מצב אתחול (מרמז -q ו -קבוצה).
-emacs אומר ל-Coq שזה מבוצע תחת Emacs.
-מזבלה-גלוב f
זרוק גלובליזציות בקובץ f (לשימוש על ידי coqdoc(1)).
-סט אימפריקטיבי
קבע מיון קבע מאפיין.
-אל תעמיס הוכחות
אל תטען הוכחות אטומות בזיכרון.
-xml ייצא קובצי XML אל ההיררכיה המושרשת בספריה
COQ_XML_LIBRARY_ROOT (אם מוגדר) או ל-stdout (אם לא מוגדר).
השתמש ב-coqide באינטרנט באמצעות שירותי onworks.net
