ນີ້ແມ່ນຄໍາສັ່ງ coqchk.opt ທີ່ສາມາດດໍາເນີນການໄດ້ໃນ OnWorks ຜູ້ໃຫ້ບໍລິການໂຮດຕິ້ງຟຣີໂດຍໃຊ້ຫນຶ່ງໃນຫຼາຍໆບ່ອນເຮັດວຽກອອນໄລນ໌ຂອງພວກເຮົາເຊັ່ນ Ubuntu Online, Fedora Online, Windows online emulator ຫຼື MAC OS online emulator
ໂຄງການ:
NAME
coqchk - The Coq Proof Checker ລວບລວມຕົວກວດສອບຫ້ອງສະໝຸດ
ສະຫຼຸບສັງລວມ
coqchk [ ທາງເລືອກໃນການ ] ໂມດູນ
ລາຍລະອຽດ
coqchk ແມ່ນຕົວກວດສອບແບບສະແຕນເລດຂອງຫ້ອງສະໝຸດທີ່ລວບລວມ (ໄຟລ໌ .vo ທີ່ຜະລິດໂດຍ coqc) ສໍາລັບ
ຜູ້ຊ່ວຍຫຼັກຖານສະແດງ Coq. ເບິ່ງຄູ່ມືອ້າງອີງສຳລັບຂໍ້ມູນເພີ່ມເຕີມ. ມັນກັບຄືນມາດ້ວຍ
ອອກຈາກລະຫັດ 0 ຖ້າທຸກວຽກທີ່ຮ້ອງຂໍສໍາເລັດ. ລະຫັດກັບຄືນທີ່ບໍ່ແມ່ນສູນຫມາຍຄວາມວ່າ
ບາງສິ່ງບາງຢ່າງຜິດພາດ: ບາງຫ້ອງສະຫມຸດບໍ່ໄດ້ພົບເຫັນ, ເນື້ອໃນຄວາມເສຍຫາຍ, ການກວດສອບປະເພດ
ຄວາມລົ້ມເຫຼວ, ແລະອື່ນໆ.
ໂມດູນ ແມ່ນບັນຊີລາຍຊື່ຂອງໂມດູນທີ່ຈະກວດສອບ. ໂມດູນສາມາດຖືກອ້າງເຖິງໂດຍຫຍໍ້ຫຼື
ຊື່ທີ່ມີຄຸນວຸດທິ.
OPTIONS
-I ແມ່ນ, --ລວມ dir
ເພີ່ມໄດເລກະທໍລີ dir ຢູ່ໃນເສັ້ນທາງລວມ
-R dir coqdir
ແຜນທີ່ທາງກາຍຍະພາບ recursively dir ກັບເຫດຜົນ coqdir
- ງຽບ
ເຮັດໃຫ້ coqchk ຫນ້ອຍ verbose.
- ຍອມຮັບ ໂມດູນ
tag ໂມດູນທີ່ລະບຸໄວ້ແລະການຂຶ້ນກັບທັງຫມົດຂອງມັນເປັນທີ່ເຊື່ອຖືໄດ້, ແລະຈະບໍ່ເປັນ
ກວດຄືນແລ້ວ, ເວັ້ນເສຍແຕ່ຈະຮ້ອງຂໍຢ່າງຈະແຈ້ງໂດຍທາງເລືອກອື່ນ.
- ໂນເຣກ ໂມດູນ
ລະບຸວ່າໂມດູນທີ່ໃຫ້ນັ້ນຈະຖືກກວດສອບໂດຍບໍ່ໄດ້ຮ້ອງຂໍໃຫ້ກວດເບິ່ງມັນ
ການເພິ່ງພາອາໄສ.
-m, -- ຄວາມຊົງຈໍາ
ສະແດງບົດສະຫຼຸບຂອງຫນ່ວຍຄວາມຈໍາທີ່ໃຊ້ໂດຍ checker.
-o, --output-context
ສະແດງຂໍ້ສັງລວມຂອງເນື້ອໃນທີ່ມີເຫດຜົນທີ່ໄດ້ຮັບການກວດສອບ: ສົມມຸດຕິຖານແລະ
ການນໍາໃຊ້ impredicativity.
- ຄາດຄະເນຊຸດ
ອະນຸຍາດໃຫ້ຜູ້ກວດກາຍອມຮັບຫ້ອງສະຫມຸດທີ່ໄດ້ຖືກລວບລວມດ້ວຍທຸງນີ້.
-v ພິມສະບັບ coqchk ແລະອອກ.
-coqlib dir
overrides ສະຖານທີ່ເລີ່ມຕົ້ນຂອງຫ້ອງສະຫມຸດມາດຕະຖານ.
- ບ່ອນໃດ ພິມສະຖານທີ່ຫ້ອງສະຫມຸດມາດຕະຖານ coqchk ແລະອອກ.
-ຊ, - ຊ່ວຍ
ພິມລາຍການທາງເລືອກ
ໃຊ້ coqchk.opt ອອນໄລນ໌ໂດຍໃຊ້ບໍລິການ onworks.net
