Đây là coqchk lệnh có thể chạy trong nhà cung cấp dịch vụ lưu trữ miễn phí OnWorks bằng cách sử dụng một trong nhiều máy trạm trực tuyến miễn phí của chúng tôi như Ubuntu Online, Fedora Online, trình giả lập trực tuyến Windows hoặc trình mô phỏng trực tuyến MAC OS
CHƯƠNG TRÌNH:
TÊN
coqchk - Trình xác minh thư viện đã biên dịch Coq Proof Checker
SYNOPSIS
coqchk [ lựa chọn ] mô-đun
MÔ TẢ
coqchk là trình kiểm tra độc lập của các thư viện đã biên dịch (tệp .vo do coqc tạo ra) cho
Trợ lý Chứng minh Coq. Xem Sổ tay Tham khảo để biết thêm thông tin. Nó trở lại với
thoát mã 0 nếu tất cả các tác vụ được yêu cầu đã thành công. Một mã trả lại khác XNUMX có nghĩa là
đã xảy ra sự cố: một số thư viện không được tìm thấy, nội dung bị hỏng, kiểm tra loại
thất bại, v.v.
mô-đun là danh sách các mô-đun cần kiểm tra. Các mô-đun có thể được gọi tắt là
tên đủ điều kiện.
LỰA CHỌN
-I Là, --bao gồm dir
thêm thư mục dir trong đường dẫn bao gồm
-R dir coqdir
lập bản đồ đệ quy vật lý dir logic coqdir
-im lặng
làm cho coqchk ít dài dòng hơn.
-thừa nhận mô-đun
gắn thẻ mô-đun được chỉ định và tất cả các phụ thuộc của nó là đáng tin cậy và sẽ không
được kiểm tra lại, trừ khi được yêu cầu rõ ràng bởi các tùy chọn khác.
-norec mô-đun
chỉ định rằng mô-đun đã cho sẽ được xác minh mà không yêu cầu kiểm tra
sự phụ thuộc.
-NS, --kỉ niệm
hiển thị tóm tắt bộ nhớ được người kiểm tra sử dụng.
-ồ, --output-bối cảnh
hiển thị tóm tắt nội dung logic đã được xác minh: các giả định và
sử dụng tính không tin cậy.
-impredicative-bộ
cho phép người kiểm tra chấp nhận các thư viện đã được biên dịch với cờ này.
-v in phiên bản coqchk và thoát.
-coqlib dir
ghi đè vị trí mặc định của thư viện chuẩn.
-ở đâu in vị trí thư viện chuẩn coqchk và thoát.
-NS, --Cứu giúp
in danh sách các tùy chọn
Sử dụng coqchk trực tuyến bằng các dịch vụ onworks.net
