.TH COQDEP 1
.
.SH "نام (NAME)"
coqdep \- محاسبه وابستگی‌های متقابل در نظریه‌ها و کدهای زبان اثبات Coq
.
.SH "خلاصه دستور (SYNOPSIS)"
.B coqdep
[
.BI \-I \ directory
]
[
.BI \-coqlib \ directory
]
[
.B \-i
]
[
.B \-slash
]
.I filename .\|.\|.\&
.I directory .\|.\|.
.
.SH "توضیحات (DESCRIPTION)"
.
دستور
.B coqdep
وابستگی‌های متقابل میان ماژول‌ها را برای برنامه‌های Coq محاسبه می‌کند
و وابستگی‌ها را با ساختاری قابل خواندن برای ابزار
.BR make
روی خروجی استاندارد چاپ می‌نماید.
هنگامی که یک دایرکتوری به عنوان آرگومان مشخص شود، به صورت بازگشتی بررسی می‌گردد.
.PP
وابستگی‌های ماژول‌های Coq با بررسی دستورات
.I Require
(دستورات Require، Require Export، Require Import، احتمالاً محدود شده با بند From)،
دستورات
.I Declare
.I ML
.I Module ,
دستورات
.I Add
.I LoadPath
و دستورات
.I Load
محاسبه می‌شوند.
وابستگی‌های مربوط به ماژول‌های کتابخانه اصلی Coq چاپ نمی‌شوند، مگر آنکه گزینه
.B \-boot
مشخص شده باشد.
.
.SH "گزینه‌ها (OPTIONS)"
.
.TP
.BI \-f \ file
خواندن نام فایل‌ها و گزینه‌های
.BR \-I ,
.B \-R
و
.B \-Q
از فایل پروژه
.IR file
(مانند _CoqProject).
.TP
.BI \-I\fR/\fB\-Q\fR/\fB\-R \ options
اعمال اثری یکسان بر مسیر بارگذاری و نام ماژول‌ها همانند سایر دستورات Coq (\c
.BR coqtop ,
.BR coqc ).
.TP
.BI \-coqlib \ directory
مشخص کردن محل قرارگیری کتابخانه Coq.
مقدار پیش‌فرض در زمان نصب برنامه تعیین شده است، بنابراین در شرایط عادی نباید از این گزینه استفاده شود.
.TP
.BI \-exclude-dir \ dir
صرف‌نظر کردن از زیردایرکتوری
.I dir
هنگام جستجو با گزینه‌های
.BR \-R / \-Q .
.TP
.B \-sort
چاپ نام فایل‌های داده‌شده بر اساس اولویت و ترتیب وابستگی‌هایشان.
.TP
.B \-vos
چاپ وابستگی‌ها برای فایل‌های .vos (این حالت پیش‌فرض نیست زیرا سازگاری حالت Coq در ابزار dune را مختل می‌کند).
.TP
.B \-boot
برای توسعه‌دهندگان Coq؛ چاپ وابستگی‌های روی فایل‌های کتابخانه اصلی Coq (به صورت پیش‌فرض چاپ نمی‌شوند).
.TP
.B \-noinit
در حال حاضر هیچ اثری ندارد.
.TP
.B \-vos
شامل کردن وابستگی‌های مرتبط با فایل‌های .vos.
.TP
.BR \-dyndep \ ( opt | byte | both | no | var )
تنظیم نحوه چاپ وابستگی‌های روی ماژول‌های ML.
.TP
.BI \-m \ meta
حل و شناسایی نام افزونه‌ها با استفاده از فایل
.IR meta .
.TP
.BI \-w \ w1,\|.\|.\|.\|,\|wn
پیکربندی نحوه نمایش هشدارها مشابه دستور
.BR coqc .
.
.SH "وضعیت خروج (EXIT STATUS)"
.IP 1
فایل مشخص‌شده در خط فرمان پیدا نشود، امکان باز کردن فایلی وجود نداشته باشد، یا خطای نگارشی (Syntax error) در یکی از دستورات شناخته‌شده توسط
.B coqdep
رخ داده باشد.
.IP 0
در تمام شرایط دیگر.
به ویژه، هنگامی که یک وابستگی یافت نشود یا گزینه نامعتبری وارد شده باشد،
.B coqdep
یک هشدار چاپ کرده و با وضعیت 0 خارج می‌شود.
.
.
.SH "همچنین ببینید (SEE ALSO)"
.
.BR ocamlc (1),
.BR coqc (1),
.BR make (1)
.
.SH "نکات (NOTES)"
.
تحلیل‌گرهای لغوی (برای Coq و OCaml) کامنت‌های تو در تو و رشته‌ها را به درستی پردازش می‌کنند.
.PP
پردازش و رفتار در مواجهه با پیوندهای نمادین (Symbolic links) ساده و ابتدایی است.
.PP
اگر دو فایل با نام یکسان در دو دایرکتوری مختلف وجود داشته باشند، یک هشدار در خروجی خطای استاندارد چاپ می‌شود.
.PP
هیچ روشی برای محدود کردن دامنه جستجوی بازگشتی دایرکتوری‌ها وجود ندارد.
.
.SH "مثال‌ها (EXAMPLES)"
.
فایل‌های زیر را (در یک دایرکتوری مشابه) در نظر بگیرید:
.RS
a.mllib، X.v، Y.v و Z.v
.RE
که در آن:
.IP \(bu 3
فایل a.mllib شامل نام‌های ماژول `B' و `C' است؛
.IP \(bu
فایل Y.v شامل دستور `Require Foo.X' است؛
.IP \(bu
فایل Z.v شامل دستورات `From Foo Require X' و `Declare ML Module "a"' است.
.PP
برای محاسبه و استخراج وابستگی‌های فایل‌های Coq:
.PP
.RS
.nf
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
.fi
.RE
.
.SH "گزارش اشکالات (BUGS)"
.
لطفاً هرگونه اشکال را به نشانی زیر گزارش دهید:
.BR https://github.com/coq/coq/issues