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