นี่คือคำสั่ง coqchk ที่สามารถเรียกใช้ในผู้ให้บริการโฮสต์ฟรีของ OnWorks โดยใช้เวิร์กสเตชันออนไลน์ฟรีของเรา เช่น Ubuntu Online, Fedora Online, โปรแกรมจำลองออนไลน์ของ Windows หรือโปรแกรมจำลองออนไลน์ของ MAC OS
โครงการ:
ชื่อ
coqchk - ตัวตรวจสอบ Coq Proof Checker ที่คอมไพล์ตัวตรวจสอบไลบรารี
เรื่องย่อ
ค็อกคคค [ ตัวเลือก ] โมดูล
DESCRIPTION
ค็อกคคค เป็นตัวตรวจสอบแบบสแตนด์อโลนของไลบรารีที่คอมไพล์แล้ว (ไฟล์ .vo ที่ผลิตโดย coqc) สำหรับ
ผู้ช่วยพิสูจน์ Coq ดูคู่มืออ้างอิงสำหรับข้อมูลเพิ่มเติม มันกลับมาพร้อมกับ
รหัสออก 0 หากงานที่ร้องขอทั้งหมดสำเร็จ รหัสส่งคืนที่ไม่ใช่ศูนย์หมายความว่า
มีบางอย่างผิดพลาด: ไม่พบไลบรารีบางตัว เนื้อหาเสียหาย การตรวจสอบประเภท
ความล้มเหลว ฯลฯ
โมดูล เป็นรายการโมดูลที่จะตรวจสอบ โมดูลสามารถอ้างถึงโดยย่อหรือ
ชื่อที่ผ่านการรับรอง
OPTIONS
-I ผบ. --รวม dir
เพิ่มไดเรกทอรี dir ในเส้นทางรวม
-R dir ค็อกเดียร์
ทำซ้ำแผนที่ทางกายภาพ dir เป็นตรรกะ ค็อกเดียร์
-เงียบ
ทำให้ coqchk ละเอียดน้อยลง
-ยอมรับ โมดูล
แท็กโมดูลที่ระบุและการพึ่งพาทั้งหมดว่าเชื่อถือได้และจะไม่
ตรวจสอบอีกครั้ง เว้นแต่จะมีการร้องขออย่างชัดเจนจากตัวเลือกอื่น
-โนเร็ก โมดูล
ระบุว่าโมดูลที่กำหนดจะต้องได้รับการตรวจสอบโดยไม่ต้องร้องขอให้ตรวจสอบ
การพึ่งพา
-NS, --หน่วยความจำ
แสดงสรุปหน่วยความจำที่ใช้โดยตัวตรวจสอบ
-o, --output-บริบท
แสดงบทสรุปของเนื้อหาเชิงตรรกะที่ได้รับการตรวจสอบแล้ว: สมมติฐานและ
การใช้อิมพรีดิเคทิวิตี
-impredicative-ชุด
อนุญาตให้ตัวตรวจสอบยอมรับไลบรารีที่คอมไพล์ด้วยแฟล็กนี้
-v พิมพ์เวอร์ชัน coqchk และออก
-โคคิวลิบ dir
แทนที่ตำแหน่งเริ่มต้นของไลบรารีมาตรฐาน
-ที่ไหน พิมพ์ตำแหน่งห้องสมุดมาตรฐาน coqchk และออก
-ชม, --ช่วยด้วย
พิมพ์รายการตัวเลือก
ใช้ coqchk ออนไลน์โดยใช้บริการ onworks.net
