coqdep - Trực tuyến trên đám mây

CHƯƠNG TRÌNH:

TÊN

coqdep - Tính toán sự phụ thuộc giữa các mô-đun cho các chương trình Coq và Caml

SYNOPSIS

coqdep [ -w ] [ -I thư mục ] [ -coqlib thư mục ] [ -c ] [ -i ] [ -D ] [ -gạch chéo ]
tên tập tin hữu ích. Cảm ơn ! thư mục hữu ích. Cảm ơn !

MÔ TẢ

coqdep tính toán các phụ thuộc giữa các mô-đun cho các chương trình Coq và Caml, và in
phụ thuộc vào đầu ra tiêu chuẩn ở định dạng có thể đọc được bởi make. Khi một thư mục là
được đưa ra dưới dạng đối số, nó được xem xét một cách đệ quy.

Sự phụ thuộc của các mô-đun Coq được tính toán bằng cách xem Yêu cầu lệnh (Yêu cầu, Yêu cầu
Xuất, Yêu cầu Nhập), Khai báo ML Mô-đun lệnh và Phụ tải các lệnh. Sự phụ thuộc
liên quan đến các mô-đun từ thư viện Coq không được in.

Sự phụ thuộc của các mô-đun Caml được tính toán bằng cách xem mở chỉ thị và dấu chấm
ký hiệu mô-đun.giá trị.

LỰA CHỌN

-c In các phần phụ thuộc của các mô-đun Caml. (Trên các mô-đun Caml, hành vi là
hoàn toàn giống với ocamldep).

-w In cảnh báo nếu lệnh Coq Khai báo ML Mô-đun là không chính xác. (Ví dụ,
bạn đã viết `Khai báo mô-đun ML" A ". ', nhưng mô-đun A chứa #open" B "). Các
lệnh đúng được in (xem tùy chọn -D). Cảnh báo được in trên tiêu chuẩn
lỗi.

-D Lệnh này tìm kiếm mọi lệnh Khai báo ML Mô-đun của mỗi tệp Coq được cung cấp dưới dạng
đối số và hoàn thành (nếu cần) danh sách các mô-đun Caml. Lệnh mới là
được in trên đầu ra tiêu chuẩn. Không có sự phụ thuộc nào được tính toán với tùy chọn này.

-gạch chéo In các đường dẫn bằng dấu gạch chéo thay vì dấu phân cách dành riêng cho hệ điều hành. Tùy chọn này là
hữu ích khi phát triển dưới Cygwin.

-I thư mục
Các tệp .v .ml .mli của thư mục thư mục được tính đến trong quá trình
tích của các phụ thuộc, nhưng các phụ thuộc của chính chúng không được in ra.

-coqlib thư mục
Cho biết thư viện Coq ở đâu. Giá trị mặc định đã được xác định tại
thời gian cài đặt, và do đó tùy chọn này không nên được sử dụng trong điều kiện bình thường
hoàn cảnh.

Sử dụng coqdep trực tuyến bằng các dịch vụ onworks.net