นี่คือคำสั่ง coqide.byte ที่สามารถเรียกใช้ในผู้ให้บริการโฮสต์ฟรีของ OnWorks โดยใช้หนึ่งในเวิร์กสเตชันออนไลน์ฟรีของเรา เช่น Ubuntu Online, Fedora Online, โปรแกรมจำลองออนไลน์ของ Windows หรือโปรแกรมจำลองออนไลน์ของ MAC OS
โครงการ:
ชื่อ
coqide - ส่วนต่อประสานกราฟิก Coq Proof Assistant
เรื่องย่อ
โคไคด์ [ ตัวเลือก ]
DESCRIPTION
โคไคด์ เป็นอินเทอร์เฟซกราฟิก gtk สำหรับผู้ช่วยพิสูจน์ Coq
สำหรับการใช้ Coq ตามบรรทัดคำสั่ง โปรดดูที่ คอคท็อป(1) ; สำหรับการใช้ Coq แบบกลุ่ม โปรดดู
ค็อกซี(1)
OPTIONS
-h แสดงรายการตัวเลือกทั้งหมดที่ยอมรับโดย โคไคด์.
-I dir, - รวม dir
เพิ่มไดเร็กทอรี dir ในพาธรวม
-R dir ค็อกเดียร์
ทำซ้ำแผนที่ทางกายภาพ dir เป็นตรรกะ ค็อกเดียร์.
-src เพิ่มไดเร็กทอรีต้นทางในพาธรวม
-คือ f, -อินพุตสถานะ f
อ่านสถานะจาก f.coq
- เสียงรบกวน เริ่มต้นด้วยสถานะว่างเปล่า
-สถานะเอาท์พุท f
เขียนสถานะในไฟล์ f.coq
-load-ml-วัตถุ f
โหลดไฟล์อ็อบเจ็กต์ ML f.
-load-ml-แหล่งที่มา f
โหลดไฟล์ ML f.
-l f, -load-vernac-แหล่งที่มา f
โหลดไฟล์ Coq f.v (โหลด f.)
-เลเวล f, -load-vernac-source-verbose f
โหลดไฟล์ Coq f.v (โหลดรายละเอียด f.)
-load-vernac-วัตถุ f
โหลดไฟล์อ็อบเจ็กต์ Coq f.vo
-จำเป็นต้อง f
โหลดไฟล์อ็อบเจ็กต์ Coq f.vo และนำเข้า (Require f.)
-รวบรวม f
รวบรวมไฟล์ Coq f.v (หมายถึง -แบทช์).
-คอมไพล์-verbose f
รวบรวมไฟล์ Coq อย่างละเอียด f.v (หมายถึง -แบทช์).
-เลือก เรียกใช้ Coq หรือ Coq_SearchIsos เวอร์ชันโค้ดเนทีฟ
-ไบต์ รันเวอร์ชัน bytecode ของ Coq หรือ Coq_SearchIsos
-ที่ไหน พิมพ์ตำแหน่งและทางออกของห้องสมุดมาตรฐานของ Coq
-v พิมพ์เวอร์ชัน Coq และออก
-q ข้ามการโหลด rcfile.js
-init-ไฟล์ f
ตั้งค่า rcfile เป็น f.
-แบทช์ โหมดแบทช์ (ออกหลังจากแยกวิเคราะห์อาร์กิวเมนต์)
- บูต โหมดบูต (หมายถึง -q และ -แบทช์).
-emac บอก Coq ว่าดำเนินการภายใต้ Emacs
-dump-โลก f
ดัมพ์โลกาภิวัตน์ในไฟล์ f (ที่จะใช้โดย ค็อกด็อก(พ.ศ. 1)).
-impredicative-ชุด
ตั้งค่าการเรียงลำดับ ตั้งค่า impredicative
-ไม่โหลดหลักฐาน
อย่าโหลดหลักฐานทึบแสงในหน่วยความจำ
-xml ส่งออกไฟล์ XML ไปยังลำดับชั้นที่รูทในไดเร็กทอรี
COQ_XML_LIBRARY_ROOT (ถ้าตั้งค่า) หรือ stdout (ถ้าไม่ได้ตั้งค่า)
ใช้ coqide.byte ออนไลน์โดยใช้บริการ onworks.net
