.TH COQCHK 1
.
.SH "نام (NAME)"
coqchk \- اعتبارسنجی کتابخانه‌های کامپایل‌شده‌ی Coq
.
.SH "خلاصه دستور (SYNOPSIS)"
.B coqchk
[
گزینه‌ها
]
.I modules
.
.SH "توضیحات (DESCRIPTION)"
.
.B coqchk
بررسی‌کننده‌ی مستقل کتابخانه‌های کامپایل‌شده (فایل‌های .vo تولیدشده توسط
.BR coqc )
برای دستیار اثبات Coq است.
برای اطلاعات بیشتر به
.I Reference Manual
مراجعه کنید.
اگر تمام وظایف درخواستی با موفقیت انجام شوند، با کد خروج 0 خارج می‌شود.
کد خروج غیرصفر نشان‌دهنده‌ی بروز خطا است: عدم یافتن کتابخانه، محتوای مخدوش، شکست در بررسی نوع (type-checking) و غیره.
.PP
.I modules
فهرستی از ماژول‌ها برای بررسی است.
ماژول‌ها می‌توانند با نام منطقی کوتاه یا کامل، یا با نام فایل آن‌ها مشخص شوند.
.
.SH "گزینه‌ها (OPTIONS)"
.
.TP
.BI \-I \ dir, \ \-\-include \ dir
افزودن دایرکتوری
.I dir
به مسیر include.
.
.TP
.BI \-Q \ dir\ coqdir
نگاشت دایرکتوری فیزیکی
.I dir
به دایرکتوری منطقی
.IR coqdir .
.
.TP
.BI \-R \ dir\ coqdir
مترادف با
.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 coqchk
و خروج.
.
.TP
.BI \-coqlib \ dir
مسیر پیش‌فرض کتابخانه‌ی استاندارد را بازنویسی می‌کند.
.
.TP
.B \-where
نمایش مکان کتابخانه‌ی استاندارد coqchk و خروج.
.
.TP
.BR \-h ,\  \-\-help
نمایش فهرست گزینه‌ها.
.
.SH "همچنین ببینید (SEE ALSO)"
.
.BR coqtop (1),
.BR coqc (1),
.BR coq_makefile (1),
.BR coqdep (1)
.PP
.I
The Rocq Prover Reference Manual.
.PP
وب‌سایت Rocq Prover: https://rocq-prover.org