.TH COQNATIVE 1
.
.SH "نام (NAME)"
coqnative \- کامپایلر بومی Coq
.
.
.SH "خلاصه دستور (SYNOPSIS)"
.B coqnative
[
گزینه‌ها
]
.I filename
.
.
.SH "توضیحات (DESCRIPTION)"
.
دستور
.B coqnative
فایل‌های vo را به فایل‌های باینری مورد استفاده توسط سازوکار محاسبه بومی (native compute) در دستیار اثبات Coq کامپایل می‌کند.
برای اطلاعات بیشتر به
.I "کتابچه راهنمای مرجع"
مراجعه کنید.
اگر تمام وظایف درخواستی با موفقیت انجام شوند، با وضعیت خروج 0 بازمی‌گردد.
کد خروج غیرصفر نشان‌دهنده بروز خطا در فرآیند است.
.PP
آرگومان
.I filename
یک فایل شیء Coq (یک فایل ‎.vo) است که باید به باینری بومی کامپایل شود.
.
.SH "گزینه‌ها (OPTIONS)"
.
.TP
.BI \-Q \ dir\ coqdir
نگاشت دایرکتوری فیزیکی
.I dir
به دایرکتوری منطقی
.I coqdir.
.
.TP
.BI \-R \ dir\ coqdir
مترادف با
.BR \-Q .
.
.TP
.BI \-I \ dir
نادیده گرفته می‌شود؛ صرفاً برای سازگاری.
.
.TP
.B \-noinit
نادیده گرفته می‌شود؛ صرفاً برای سازگاری.
.
.TP
.B \-boot
حالت راه‌اندازی (Boot mode).
.
.TP
.BI \-coqlib \ dir
جایگزین کردن مکان پیش‌فرض کتابخانه استاندارد.
.
.TP
.BI \-nI \ dir
افزودن
.I dir
به مجموعه مسیرهای مربوط به فایل‌های بومی وابستگی‌ها.
.
.TP
.BI \-native-output-dir \ dir
ذخیره فایل‌های تولیدشده در دایرکتوری
.I dir.
.
.TP
.BR \-h , \ \-\-help
نمایش فهرست گزینه‌ها.
.
.SH "همچنین ببینید (SEE ALSO)"
.
.BR coqtop (1),
.BR coqc (1),
.BR coq_makefile (1),
.BR coqdep (1)
.PP
.I
کتابچه راهنمای مرجع Rocq Prover.
.PP
وب‌سایت Rocq Prover: https://rocq-prover.org