| ROCQIDE(1) | General Commands Manual | ROCQIDE(1) |
نام (NAME)
rocqide - رابط گرافیکی برای Rocq Prover
خلاصه دستور (SYNOPSIS)
rocqide [ گزینه‌ها ]
توضیحات (DESCRIPTION)
rocqide یک رابط گرافیکی مبتنی بر GTK برای Rocq Prover است.
برای استفاده از Rocq در خط فرمان یا به صورت دسته‌ای (batch)، به rocq(1) مراجعه کنید.
گزینه‌ها (OPTIONS)
- -h
- نمایش فهرست کامل گزینه‌های پذیرفته‌شده توسط rocqide.
- -I dir, -include dir
- افزودن دایرکتوری dir به مسیر include.
- -R dir rocqdir
- نگاشت بازگشتی دایرکتوری فیزیکی dir به دایرکتوری منطقی rocqdir.
- -src
- افزودن دایرکتوری‌های منبع به مسیر include.
- -nois
- شروع با یک وضعیت خالی.
- -load-ml-object f
- بارگذاری فایل شیء ML به نام f.
- -load-ml-source f
- بارگذاری فایل منبع ML به نام f.
- -l f, -load-vernac-source f
- بارگذاری فایل Rocq به نام f.v (Load f.).
- -lv f, -load-vernac-source-verbose f
- بارگذاری با جزئیات فایل Rocq به نام f.v (Load Verbose f.).
- -load-vernac-object path
- بارگذاری کتابخانه Rocq از مسیر path (Require path.).
- -require-import path
- بارگذاری کتابخانه Rocq از مسیر path و وارد کردن آن (Require Import path.).
- -compile f
- کامپایل فایل Rocq به نام f.v (مستلزم -batch است).
- -compile-verbose f
- کامپایل با جزئیات فایل Rocq به نام f.v (مستلزم -batch است).
- -where
- چاپ مسیر کتابخانه استاندارد Rocq و خروج.
- -v
- چاپ نسخه Rocq و خروج.
- -q
- صرف‌نظر از بارگذاری rcfile.
- -init-file f
- تنظیم rcfile به f.
- -emacs
- اعلام به Rocq مبنی بر اینکه تحت Emacs اجرا می‌شود.
- -dump-glob f
- ذخیره ارجاعات سراسری در فایل f (جهت استفاده توسط rocq(1)doc).
- -impredicative-set
- تنظیم مرتبه (sort) Set به حالت impredicative.
- -dont-load-proofs
- عدم بارگذاری اثبات‌های مات (opaque proofs) در حافظه.
همچنین ببینید (SEE ALSO)
راهنمای مرجع Rocq
وب‌سایت Coq: http://coq.inria.fr
/usr/share/doc/rocqide/FAQ
نویسندگان (AUTHORS)
این صفحه راهنما توسط Samuel Mimram <samuel.mimram@ens-lyon.org> برای پروژه دبیان نوشته شده است (اما ممکن است توسط دیگران نیز استفاده شود).