.TH COQC 1
.
.SH "نام (NAME)"
coqc \- کامپایلر Coq
.
.
.SH "خلاصه دستور (SYNOPSIS)"
.B coqc
[
گزینه‌های عمومی Coq
]
.I file
.
.
.SH "توضیحات (DESCRIPTION)"
.
.B coqc
کامپایلر دسته‌ای (batch) برای دستیار اثبات Coq است.
گزینه‌ها اساساً مشابه
.BR coqtop (1)
هستند.
.I file.v
فایل vernacular برای کامپایل است.
.I file
باید تنها از
نویسه‌های «a» تا «Z»، «0» تا «9» یا «_» تشکیل شده باشد و باید با یک حرف
آغاز شود.
کامپایلر یک فایل شیء
.IR file.vo \&
تولید می‌کند.
.PP
برای استفادهٔ تعاملی از Coq، به
.BR coqtop (1)
مراجعه کنید.
.
.
.SH "گزینه‌ها (OPTIONS)"
.
.\" TODO: Coqc is not a script.  Correct this claim.
.B coqc
اسکریپتی است که صرفاً
.B coqtop
را با گزینهٔ
.BR \-compile
اجرا می‌کند. این ابزار همان گزینه‌های
.BR coqtop
را می‌پذیرد.
.
.TP
.BI \-image \ bin
استفاده از
.I bin
به‌عنوان
.B coqtop
زیربنایی به‌جای نمونهٔ پیش‌فرض.
.
.TP
.B \-verbose
چاپ فایل کامپایل‌شده روی خروجی استاندارد.
.
.SH "همچنین ببینید (SEE ALSO)"
.
.BR coqtop (1),
.BR coq_makefile (1),
.BR coqdep (1)
.PP
.I
راهنمای مرجع اثبات‌گر Rocq (The Rocq Prover Reference Manual).
.PP
وب‌سایت اثبات‌گر Rocq: https://rocq-prover.org