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)
       rocq(1),

       The Rocq Reference Manual.

       وب‌سایت Rocq: http://coq.inria.fr

                                                                    ROCQCHK(1)