นี่คือคำสั่ง coqdep ที่สามารถเรียกใช้ในผู้ให้บริการโฮสต์ฟรีของ OnWorks โดยใช้เวิร์กสเตชันออนไลน์ฟรีของเรา เช่น Ubuntu Online, Fedora Online, โปรแกรมจำลองออนไลน์ของ Windows หรือโปรแกรมจำลองออนไลน์ของ MAC OS
โครงการ:
ชื่อ
coqdep - คำนวณการพึ่งพาระหว่างโมดูลสำหรับโปรแกรม Coq และ Caml
เรื่องย่อ
ค็อกเดป [ -w ] [ -I ไดเรกทอรี ] [ -โคคิวลิบ ไดเรกทอรี ] [ -c ] [ -i ] [ -D ] [ - สแลช ]
ชื่อไฟล์ ... ไดเรกทอรี ...
DESCRIPTION
ค็อกเดป คำนวณการพึ่งพาระหว่างโมดูลสำหรับโปรแกรม Coq และ Caml และพิมพ์
การพึ่งพาเอาต์พุตมาตรฐานในรูปแบบที่อ่านได้โดย make เมื่อไดเร็กทอรีเป็น
ให้เป็นอาร์กิวเมนต์ มันถูกมองซ้ำ ๆ
การพึ่งพาโมดูล Coq คำนวณโดยดูที่ ต้องการ คำสั่ง (Require, Require
ส่งออกต้องนำเข้า) ประกาศ ML โมดูล คำสั่งและ โหลด คำสั่ง การพึ่งพา
สัมพันธ์กับโมดูลจากไลบรารี Coq จะไม่ถูกพิมพ์
การพึ่งพาโมดูล Caml คำนวณโดยดูที่ เปิด คำสั่งและจุด
เอกสาร โมดูล.value.
OPTIONS
-c พิมพ์การอ้างอิงของโมดูล Caml (ในโมดูล Caml ลักษณะการทำงานคือ
เหมือนกับ ocamldep)
-w พิมพ์คำเตือนหากคำสั่ง Coq ประกาศ ML โมดูล ไม่ถูกต้อง (เช่น
คุณเขียนว่า 'ประกาศโมดูล ML "A" แต่โมดูล A มี #open "B") NS
พิมพ์คำสั่งที่ถูกต้อง (ดูตัวเลือก -D) คำเตือนพิมพ์บนมาตรฐาน
ความผิดพลาด
-D คำสั่งนี้จะค้นหาทุกคำสั่ง ประกาศ ML โมดูล ของแต่ละไฟล์ Coq ที่กำหนดเป็น
อาร์กิวเมนต์และกรอก (ถ้าจำเป็น) รายการโมดูล Caml คำสั่งใหม่คือ
พิมพ์บนเอาต์พุตมาตรฐาน ไม่มีการคำนวณการพึ่งพาด้วยตัวเลือกนี้
- สแลช พิมพ์เส้นทางโดยใช้เครื่องหมายทับแทนตัวคั่นเฉพาะระบบปฏิบัติการ ตัวเลือกนี้คือ
มีประโยชน์เมื่อพัฒนาภายใต้ Cygwin
-I ไดเรกทอรี
ไฟล์ .v .ml .mli ของไดเร็กทอรี ไดเรกทอรี จะถูกนำมาพิจารณาในระหว่าง
แคลคูลัสของการพึ่งพา แต่ไม่มีการพิมพ์การพึ่งพาของตัวเอง
-โคคิวลิบ ไดเรกทอรี
ระบุว่าไลบรารี Coq อยู่ที่ไหน ค่าเริ่มต้นถูกกำหนดไว้ที่
เวลาติดตั้ง ดังนั้นจึงไม่ควรใช้ตัวเลือกนี้ภายใต้สภาวะปกติ
พฤติการณ์
ใช้ coqdep ออนไลน์โดยใช้บริการ onworks.net
