| COQC(1) | General Commands Manual | COQC(1) |
نام (NAME)
coqc - کامپایلر Coq
خلاصه دستور (SYNOPSIS)
coqc [ گزینه‌های عمومی Coq ] file
توضیحات (DESCRIPTION)
coqc کامپایلر دسته‌ای (batch) برای دستیار اثبات Coq است. گزینه‌ها اساساً مشابه coqtop(1) هستند. file.v فایل vernacular برای کامپایل است. file باید تنها از نویسه‌های «a» تا «Z»، «0» تا «9» یا «_» تشکیل شده باشد و باید با یک حرف آغاز شود. کامپایلر یک فایل شیء file.vo تولید می‌کند.
برای استفادهٔ تعاملی از Coq، به coqtop(1) مراجعه کنید.
گزینه‌ها (OPTIONS)
coqc اسکریپتی است که صرفاً coqtop را با گزینهٔ -compile اجرا می‌کند. این ابزار همان گزینه‌های coqtop را می‌پذیرد.
- -image bin
- استفاده از bin به‌عنوان coqtop زیربنایی به‌جای نمونهٔ پیش‌فرض.
- -verbose
- چاپ فایل کامپایل‌شده روی خروجی استاندارد.
همچنین ببینید (SEE ALSO)
coqtop(1), coq_makefile(1), coqdep(1)
راهنمای مرجع اثبات‌گر Rocq (The Rocq Prover Reference Manual).
وب‌سایت اثبات‌گر Rocq: https://rocq-prover.org