ນີ້ແມ່ນຄໍາສັ່ງ coqdep ທີ່ສາມາດດໍາເນີນການໄດ້ໃນ OnWorks ຜູ້ໃຫ້ບໍລິການໂຮດຕິ້ງຟຣີໂດຍໃຊ້ຫນຶ່ງໃນຫຼາຍໆບ່ອນເຮັດວຽກອອນໄລນ໌ຂອງພວກເຮົາເຊັ່ນ Ubuntu Online, Fedora Online, Windows online emulator ຫຼື MAC OS online emulator
ໂຄງການ:
NAME
coqdep - ການຂຶ້ນກັບໂມດູນລະຫວ່າງຄອມພິວເຕີສໍາລັບໂຄງການ Coq ແລະ Caml
ສະຫຼຸບສັງລວມ
coqdep [ -w ] [ -I ລະບົບ ] [ -coqlib ລະບົບ ] [ -c ] [ -i ] [ -D ] [ -slash ]
ຊື່ເອກະສານ ... ລະບົບ ...
ລາຍລະອຽດ
coqdep compute inter-module dependencies ສໍາລັບໂຄງການ Coq ແລະ Caml, ແລະພິມ
ຂຶ້ນກັບຜົນຜະລິດມາດຕະຖານໃນຮູບແບບທີ່ສາມາດອ່ານໄດ້ໂດຍການເຮັດໃຫ້. ເມື່ອໄດເລກະທໍລີແມ່ນ
ໃຫ້ເປັນການໂຕ້ຖຽງ, ມັນຖືກເບິ່ງຄືນຢູ່.
ຄວາມເພິ່ງພາອາໄສຂອງໂມດູນ Coq ຖືກຄິດໄລ່ໂດຍການເບິ່ງ ຕ້ອງການ ຄໍາສັ່ງ (Require, Require
ສົ່ງອອກ, ຕ້ອງການນໍາເຂົ້າ), ປະກາດ ML ໂມດູນ ຄໍາສັ່ງແລະ Load ຄໍາສັ່ງ. ການເພິ່ງພາອາໄສ
ກ່ຽວຂ້ອງກັບໂມດູນຈາກຫ້ອງສະຫມຸດ Coq ບໍ່ໄດ້ຖືກພິມອອກ.
ຄວາມເພິ່ງພາອາໄສຂອງໂມດູນ Caml ຖືກຄິດໄລ່ໂດຍການເບິ່ງ ເປີດ ທິດທາງແລະຈຸດ
ຄະແນນ module.value.
OPTIONS
-c ພິມຄວາມຂຶ້ນກັບຂອງໂມດູນ Caml. (ໃນໂມດູນ Caml, ພຶດຕິກໍາແມ່ນ
ຄືກັນກັບ ocamldep).
-w ພິມຄໍາເຕືອນຖ້າຫາກວ່າຄໍາສັ່ງ Coq ປະກາດ ML ໂມດູນ ບໍ່ຖືກຕ້ອງ. (ຕົວຢ່າງ,
ທ່ານຂຽນວ່າ 'ປະກາດ ML Module "A".', ແຕ່ໂມດູນ A ມີ #open "B"). ໄດ້
ຄໍາສັ່ງທີ່ຖືກຕ້ອງຖືກພິມອອກ (ເບິ່ງທາງເລືອກ -D). ຄໍາເຕືອນແມ່ນພິມຕາມມາດຕະຖານ
ຜິດພາດ.
-D ຄໍາສັ່ງນີ້ຊອກຫາທຸກຄໍາສັ່ງ ປະກາດ ML ໂມດູນ ຂອງແຕ່ລະໄຟລ໌ Coq ໃຫ້ເປັນ
ການໂຕ້ຖຽງແລະສໍາເລັດ (ຖ້າຈໍາເປັນ) ບັນຊີລາຍຊື່ຂອງໂມດູນ Caml. ຄໍາສັ່ງໃຫມ່ແມ່ນ
ພິມຢູ່ໃນຜົນຜະລິດມາດຕະຖານ. ບໍ່ມີການເພິ່ງພາອາໄສທາງເລືອກນີ້.
-slash ພິມເສັ້ນທາງໂດຍໃຊ້ເຄື່ອງໝາຍທັບແທນຕົວແຍກສະເພາະ OS. ທາງເລືອກນີ້ແມ່ນ
ເປັນປະໂຫຍດໃນເວລາທີ່ການພັດທະນາພາຍໃຕ້ Cygwin.
-I ລະບົບ
ໄຟລ໌ .v .ml .mli ຂອງໄດເລກະທໍລີ ລະບົບ ໄດ້ຖືກພິຈາລະນາໃນລະຫວ່າງ
calculus ຂອງ dependencies, ແຕ່ dependencies ຂອງເຂົາເຈົ້າເອງຍັງບໍ່ໄດ້ພິມອອກ.
-coqlib ລະບົບ
ຊີ້ບອກວ່າຫ້ອງສະໝຸດ Coq ຢູ່ໃສ. ຄ່າເລີ່ມຕົ້ນໄດ້ຖືກກໍານົດຢູ່ທີ່
ເວລາຕິດຕັ້ງ, ແລະດັ່ງນັ້ນທາງເລືອກນີ້ບໍ່ຄວນຖືກນໍາໃຊ້ພາຍໃຕ້ປົກກະຕິ
ສະຖານະການ.
ໃຊ້ coqdep ອອນໄລນ໌ໂດຍໃຊ້ບໍລິການ onworks.net