coqchk.opt - ออนไลน์ใน Cloud

โครงการ:

ชื่อ

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.opt ออนไลน์โดยใช้บริการ onworks.net