| 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