نام (NAME)

coqdep - محاسبه وابستگی‌های متقابل در نظریه‌ها و کدهای زبان اثبات Coq

خلاصه دستور (SYNOPSIS)

coqdep [ -I directory ] [ -coqlib directory ] [ -i ] [ -slash ] filename ... directory ...

توضیحات (DESCRIPTION)

دستور coqdep وابستگی‌های متقابل میان ماژول‌ها را برای برنامه‌های Coq محاسبه می‌کند و وابستگی‌ها را با ساختاری قابل خواندن برای ابزار make روی خروجی استاندارد چاپ می‌نماید. هنگامی که یک دایرکتوری به عنوان آرگومان مشخص شود، به صورت بازگشتی بررسی می‌گردد.

وابستگی‌های ماژول‌های Coq با بررسی دستورات Require (دستورات Require، Require Export، Require Import، احتمالاً محدود شده با بند From)، دستورات Declare ML Module , دستورات Add LoadPath و دستورات Load محاسبه می‌شوند. وابستگی‌های مربوط به ماژول‌های کتابخانه اصلی Coq چاپ نمی‌شوند، مگر آنکه گزینه -boot مشخص شده باشد.

گزینه‌ها (OPTIONS)

-f file: خواندن نام فایل‌ها و گزینه‌های -I, -R و -Q از فایل پروژه file (مانند _CoqProject).
-I/-Q/-R options: اعمال اثری یکسان بر مسیر بارگذاری و نام ماژول‌ها همانند سایر دستورات Coq (coqtop, coqc).
-coqlib directory: مشخص کردن محل قرارگیری کتابخانه Coq. مقدار پیش‌فرض در زمان نصب برنامه تعیین شده است، بنابراین در شرایط عادی نباید از این گزینه استفاده شود.
-exclude-dir dir: صرف‌نظر کردن از زیردایرکتوری dir هنگام جستجو با گزینه‌های -R/-Q.
-sort: چاپ نام فایل‌های داده‌شده بر اساس اولویت و ترتیب وابستگی‌هایشان.
-vos: چاپ وابستگی‌ها برای فایل‌های .vos (این حالت پیش‌فرض نیست زیرا سازگاری حالت Coq در ابزار dune را مختل می‌کند).
-boot: برای توسعه‌دهندگان Coq؛ چاپ وابستگی‌های روی فایل‌های کتابخانه اصلی Coq (به صورت پیش‌فرض چاپ نمی‌شوند).
-noinit: در حال حاضر هیچ اثری ندارد.
-vos: شامل کردن وابستگی‌های مرتبط با فایل‌های .vos.
-dyndep (opt|byte|both|no|var): تنظیم نحوه چاپ وابستگی‌های روی ماژول‌های ML.
-m meta: حل و شناسایی نام افزونه‌ها با استفاده از فایل meta.
-w w1,...,wn: پیکربندی نحوه نمایش هشدارها مشابه دستور coqc.

وضعیت خروج (EXIT STATUS)

1: فایل مشخص‌شده در خط فرمان پیدا نشود، امکان باز کردن فایلی وجود نداشته باشد، یا خطای نگارشی (Syntax error) در یکی از دستورات شناخته‌شده توسط coqdep رخ داده باشد.
0: در تمام شرایط دیگر. به ویژه، هنگامی که یک وابستگی یافت نشود یا گزینه نامعتبری وارد شده باشد، coqdep یک هشدار چاپ کرده و با وضعیت 0 خارج می‌شود.

همچنین ببینید (SEE ALSO)

ocamlc(1), coqc(1), make(1)

نکات (NOTES)

تحلیل‌گرهای لغوی (برای Coq و OCaml) کامنت‌های تو در تو و رشته‌ها را به درستی پردازش می‌کنند.

پردازش و رفتار در مواجهه با پیوندهای نمادین (Symbolic links) ساده و ابتدایی است.

اگر دو فایل با نام یکسان در دو دایرکتوری مختلف وجود داشته باشند، یک هشدار در خروجی خطای استاندارد چاپ می‌شود.

هیچ روشی برای محدود کردن دامنه جستجوی بازگشتی دایرکتوری‌ها وجود ندارد.

مثال‌ها (EXAMPLES)

فایل‌های زیر را (در یک دایرکتوری مشابه) در نظر بگیرید:

a.mllib، X.v، Y.v و Z.v

که در آن:

فایل a.mllib شامل نام‌های ماژول `B' و `C' است؛
فایل Y.v شامل دستور `Require Foo.X' است؛
فایل Z.v شامل دستورات `From Foo Require X' و `Declare ML Module "a"' است.

برای محاسبه و استخراج وابستگی‌های فایل‌های Coq:

example% coqdep -I . -Q . Foo *.v
X.vo X.glob X.v.beautified X.required_vo: X.v
Y.vo Y.glob Y.v.beautified Y.required_vo: Y.v X.vo
Z.vo Z.glob Z.v.beautified Z.required_vo: Z.v X.vo ./a.cma ./a.cmxs

گزارش اشکالات (BUGS)

لطفاً هرگونه اشکال را به نشانی زیر گزارش دهید: https://github.com/coq/coq/issues