Đây là lệnh coqmktop 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 giả lập trực tuyến MAC OS
CHƯƠNG TRÌNH:
TÊN
coqmktop - Trình liên kết chiến thuật người dùng Coq Proof Assistant
SYNOPSIS
coqmktop [ lựa chọn ] các tập tin
MÔ TẢ
coqmktop xây dựng một Coq toplevel mới được mở rộng với các chiến thuật của người dùng. các tập tin là mục tiêu
Đối tượng Caml hoặc các tệp thư viện (tức là với hậu tố .cmo, .cmx, .cma hoặc .cmxa) để liên kết với
Hệ thống Coq. Trình liên kết tạo ra một toplevel Coq có thể thực thi được có thể được gọi trực tiếp
hay thông qua coqc(1), sử dụng tùy chọn -image.
LỰA CHỌN
-h Cứu giúp. Liệt kê các tùy chọn có sẵn.
-srcdir dir
Chỉ định vị trí của các tệp nguồn Coq
-o tập tin thực thi
Chỉ định tên của toplevel kết quả
-opt Biên dịch bằng mã gốc
-đầy Liên kết các chiến thuật cấp cao
-hàng đầu Xây dựng Coq trên ocaml toplevel (không tương thích với -opt)
-R dir Chỉ định các thư mục đệ quy cho Ocaml
-V8 Liên kết với ngữ pháp V8
Sử dụng coqmktop trực tuyến bằng các dịch vụ onworks.net
