นี่คือคำสั่ง coqmktop ที่สามารถเรียกใช้ในผู้ให้บริการโฮสติ้งฟรีของ OnWorks โดยใช้หนึ่งในเวิร์กสเตชันออนไลน์ฟรีของเรา เช่น Ubuntu Online, Fedora Online, โปรแกรมจำลองออนไลน์ของ Windows หรือโปรแกรมจำลองออนไลน์ของ MAC OS
โครงการ:
ชื่อ
coqmktop - ตัวเชื่อมโยงกลยุทธ์ผู้ใช้ Coq Proof Assistant
เรื่องย่อ
คอมท็อป [ ตัวเลือก ] ไฟล์
DESCRIPTION
คอมท็อป สร้าง Coq ระดับบนสุดที่ขยายด้วยกลยุทธ์ผู้ใช้ ไฟล์ คือวัตถุประสงค์
ไฟล์ออบเจ็กต์ Caml หรือไลบรารี (เช่น ต่อท้าย .cmo, .cmx, .cma หรือ .cmxa) เพื่อเชื่อมโยงกับ
ระบบโค้ก ตัวเชื่อมโยงสร้าง Coq ระดับบนสุดที่สามารถเรียกใช้งานได้โดยตรง
หรือผ่าน ค็อกซี(1) โดยใช้ตัวเลือก -image
OPTIONS
-h ช่วย. แสดงรายการตัวเลือกที่มี
-srcdir dir
ระบุว่าไฟล์ต้นทาง Coq อยู่ที่ใด
-o ไฟล์ exec
ระบุชื่อของระดับบนสุดที่เป็นผลลัพธ์
-เลือก รวบรวมในโค้ดเนทีฟ
-เต็ม เชื่อมโยงกลยุทธ์ระดับสูง
-TOP สร้าง Coq บน ocaml ระดับบนสุด (เข้ากันไม่ได้กับ -เลือก)
-R dir ระบุไดเร็กทอรีแบบเรียกซ้ำสำหรับOcaml
-v8 ลิงก์กับไวยากรณ์ V8
ใช้ coqmktop ออนไลน์โดยใช้บริการ onworks.net
