| ROCQCHK(1) | General Commands Manual | ROCQCHK(1) |
نام (NAME)
rocqchk - اعتبارسنجی کتابخانه‌های کامپایل‌شده‌ی Rocq
خلاصه دستور (SYNOPSIS)
rocqchk [ options ] modules
توضیحات (DESCRIPTION)
دستور rocqchk بررسی‌کننده‌ی مستقل کتابخانه‌های کامپایل‌شده (فایل‌های .vo تولیدشده توسط rocqcompile) برای اثبات‌کننده‌ی قضیه‌ی Rocq (Rocq Prover) است. برای اطلاعات بیشتر به Reference Manual مراجعه کنید. اگر تمامی وظایف درخواستی با موفقیت انجام شوند، با کد خروج ۰ بازمی‌گردد. کد بازگشتی غیر صفر به این معنی است که مشکلی پیش آمده است: کتابخانه‌ای پیدا نشده، محتوا خراب شده، اعتبارسنجی نوع‌ها (type-checking) شکست خورده، و غیره.
آرگومان modules فهرستی از ماژول‌ها برای بررسی است. ماژول‌ها را می‌توان با نام منطقی کوتاه، نام منطقی کامل (qualified)، یا از طریق نام فایل آن‌ها مشخص کرد.
گزینه‌ها (OPTIONS)
- -I dir, --include dir
- افزودن دایرکتوری dir به مسیر include.
- -Q dir rocqdir
- نگاشت دایرکتوری فیزیکی dir به مسیر منطقی rocqdir.
- -R dir rocqdir
- مترادف با -Q.
- -silent
- کاهش پرگویی در خروجی.
- -admit module
- ماژول مشخص‌شده و تمام وابستگی‌های آن را به عنوان مورد اعتماد علامت‌گذاری می‌کند و مجدداً بررسی نخواهند شد، مگر اینکه صریحاً توسط گزینه‌های دیگر درخواست شود.
- -norec module
- مشخص می‌کند که ماژول داده‌شده باید بدون درخواست برای بررسی وابستگی‌هایش اعتبارسنجی شود.
- -m, --memory
- نمایش خلاصه‌ای از حافظه‌ی استفاده‌شده توسط بررسی‌کننده.
- -o, --output-context
- نمایش خلاصه‌ای از محتوای منطقی اعتبارسنجی‌شده: فرضیات و استفاده از impredicativity.
- -impredicative-set
- به بررسی‌کننده اجازه می‌دهد کتابخانه‌هایی را که با این فلگ کامپایل شده‌اند بپذیرد.
- -v
- چاپ نسخه‌ی rocqchk و خروج.
- -coqlib dir
- جایگزینی مکان پیش‌فرض کتابخانه‌ی استاندارد.
- -where
- چاپ مکان کتابخانه‌ی استاندارد rocqchk و خروج.
- -h, --help
- چاپ فهرست گزینه‌ها.
همچنین ببینید (SEE ALSO)
The Rocq Reference Manual.
وب‌سایت Rocq: http://coq.inria.fr