این دستور coqchk است که می تواند در ارائه دهنده هاست رایگان OnWorks با استفاده از یکی از چندین ایستگاه کاری آنلاین رایگان مانند Ubuntu Online، Fedora Online، شبیه ساز آنلاین ویندوز یا شبیه ساز آنلاین MAC OS اجرا شود.
برنامه:
نام
coqchk - تأییدکننده کتابخانه‌های Coq Proof Checker
خلاصه
کوکچک [ گزینه های ] ماژول ها
شرح
کوکچک جستجوگر مستقل کتابخانه های کامپایل شده (فایل های vo تولید شده توسط coqc) برای است
دستیار اثبات Coq. برای اطلاعات بیشتر به کتابچه راهنمای مرجع مراجعه کنید. با آن برمی گردد
در صورت موفقیت آمیز بودن تمام وظایف درخواستی، کد خروج 0 را از آن خارج کنید. کد بازگشتی غیر صفر به این معنی است
مشکلی پیش آمد: برخی از کتابخانه ها یافت نشد، محتوای خراب، بررسی نوع
شکست و غیره
ماژول ها لیستی از ماژول هایی است که باید بررسی شوند. ماژول ها را می توان با یک یا کوتاه اشاره کرد
نام واجد شرایط
OPTIONS
-I dir ، --عبارتند از دیر
اضافه کردن دایرکتوری دیر در مسیر شامل
-R دیر coqdir
نقشه فیزیکی بازگشتی دیر به منطقی coqdir
-بی صدا
کوکچک را کمتر پرحرف می کند.
-اقرار کردن واحد
ماژول مشخص شده و همه وابستگی های آن را به عنوان مورد اعتماد تگ کنید و نخواهد بود
دوباره بررسی شد، مگر اینکه به صراحت توسط گزینه های دیگر درخواست شده باشد.
-نورک واحد
مشخص می کند که ماژول داده شده باید بدون درخواست بررسی آن تأیید شود
وابستگی ها
-m، -- حافظه
خلاصه ای از حافظه استفاده شده توسط چک کننده را نمایش می دهد.
-و ، -- خروجی - زمینه
خلاصه ای از محتوای منطقی را نشان می دهد که تأیید شده است: فرضیات و
استفاده از غیر واقعی بودن
-مجموعه-محتمل
به جستجوگر اجازه می دهد تا کتابخانه هایی را که با این پرچم کامپایل شده اند بپذیرد.
-v نسخه coqchk را چاپ کنید و خارج شوید.
-کوقلیب دیر
مکان پیش فرض کتابخانه استاندارد را لغو می کند.
-جایی که چاپ محل کتابخانه استاندارد coqchk و خروج.
-h، --کمک
چاپ لیست گزینه ها
با استفاده از خدمات onworks.net از coqchk به صورت آنلاین استفاده کنید
