| COQCHK(1) | General Commands Manual | COQCHK(1) |
نام (NAME)
coqchk - اعتبارسنجی کتابخانه‌های کامپایل‌شده‌ی Coq
خلاصه دستور (SYNOPSIS)
coqchk [ گزینه‌ها ] modules
توضیحات (DESCRIPTION)
coqchk بررسی‌کننده‌ی مستقل کتابخانه‌های کامپایل‌شده (فایل‌های .vo تولیدشده توسط coqc) برای دستیار اثبات Coq است. برای اطلاعات بیشتر به Reference Manual مراجعه کنید. اگر تمام وظایف درخواستی با موفقیت انجام شوند، با کد خروج 0 خارج می‌شود. کد خروج غیرصفر نشان‌دهنده‌ی بروز خطا است: عدم یافتن کتابخانه، محتوای مخدوش، شکست در بررسی نوع (type-checking) و غیره.
modules فهرستی از ماژول‌ها برای بررسی است. ماژول‌ها می‌توانند با نام منطقی کوتاه یا کامل، یا با نام فایل آن‌ها مشخص شوند.
گزینه‌ها (OPTIONS)
- -I dir, --include dir
- افزودن دایرکتوری dir به مسیر include.
- -Q dir coqdir
- نگاشت دایرکتوری فیزیکی dir به دایرکتوری منطقی coqdir.
- -R dir coqdir
- مترادف با -Q.
- -silent
- کاهش پیام‌های خروجی و پرگویی.
- -admit module
- ماژول مشخص‌شده و تمام وابستگی‌های آن را به عنوان قابل اعتماد علامت‌گذاری می‌کند و مجدداً بررسی نخواهند شد، مگر اینکه صراحتاً توسط گزینه‌های دیگر درخواست شده باشد.
- -norec module
- مشخص می‌کند که ماژول داده‌شده باید بدون درخواست برای بررسی وابستگی‌های آن اعتبارسنجی شود.
- -m, --memory
- خلاصه‌ای از حافظه‌ی مصرفی بررسی‌کننده را نمایش می‌دهد.
- -o, --output-context
- خلاصه‌ای از محتوای منطقی بررسی‌شده را نمایش می‌دهد: فرضیات و استفاده از impredicativity.
- -impredicative-set
- به بررسی‌کننده اجازه می‌دهد کتابخانه‌هایی را که با این فلگ کامپایل شده‌اند بپذیرد.
- -v
- نمایش نسخه‌ی coqchk و خروج.
- -coqlib dir
- مسیر پیش‌فرض کتابخانه‌ی استاندارد را بازنویسی می‌کند.
- -where
- نمایش مکان کتابخانه‌ی استاندارد coqchk و خروج.
- -h, --help
- نمایش فهرست گزینه‌ها.
همچنین ببینید (SEE ALSO)
coqtop(1), coqc(1), coq_makefile(1), coqdep(1)
The Rocq Prover Reference Manual.
وب‌سایت Rocq Prover: https://rocq-prover.org