COQNATIVE(1)                General Commands Manual               COQNATIVE(1)

نام (NAME)
       coqnative - کامپایلر بومی Coq

خلاصه دستور (SYNOPSIS)
       coqnative [ گزینه‌ها ] filename

توضیحات (DESCRIPTION)
       دستور coqnative فایل‌های vo را به فایل‌های باینری مورد استفاده توسط
       سازوکار محاسبه بومی (native compute) در دستیار اثبات Coq کامپایل می‌کند.
       برای اطلاعات بیشتر به کتابچه راهنمای مرجع مراجعه کنید.  اگر تمام وظایف
       درخواستی با موفقیت انجام شوند، با وضعیت خروج 0 بازمی‌گردد.  کد خروج
       غیرصفر نشان‌دهنده بروز خطا در فرآیند است.

       آرگومان filename یک فایل شیء Coq (یک فایل ‎.vo) است که باید به باینری
       بومی کامپایل شود.

گزینه‌ها (OPTIONS)
       -Q dir coqdir
              نگاشت دایرکتوری فیزیکی dir به دایرکتوری منطقی coqdir.

       -R dir coqdir
              مترادف با -Q.

       -I dir نادیده گرفته می‌شود؛ صرفاً برای سازگاری.

       -noinit
              نادیده گرفته می‌شود؛ صرفاً برای سازگاری.

       -boot  حالت راه‌اندازی (Boot mode).

       -coqlib dir
              جایگزین کردن مکان پیش‌فرض کتابخانه استاندارد.

       -nI dir
              افزودن dir به مجموعه مسیرهای مربوط به فایل‌های بومی وابستگی‌ها.

       -native-output-dir dir
              ذخیره فایل‌های تولیدشده در دایرکتوری dir.

       -h, --help
              نمایش فهرست گزینه‌ها.

همچنین ببینید (SEE ALSO)
       coqtop(1), coqc(1), coq_makefile(1), coqdep(1)

       کتابچه راهنمای مرجع Rocq Prover.

       وب‌سایت Rocq Prover: https://rocq-prover.org

                                                                  COQNATIVE(1)