coqtop - ອອນລາຍໃນຄລາວ

ໂຄງການ:

NAME

coqtop - ລະບົບຊັ້ນສູງຂອງຜູ້ຊ່ວຍຫຼັກຖານສະແດງ Coq

ສະຫຼຸບສັງລວມ

coqtop [ ທາງເລືອກໃນການ ]

ລາຍລະອຽດ

coqtop ແມ່ນລະບົບລະດັບສູງສຸດຂອງ Coq, ສໍາລັບການນໍາໃຊ້ແບບໂຕ້ຕອບ. ມັນອ່ານປະໂຫຍກກ່ຽວກັບ
ວັດສະດຸປ້ອນມາດຕະຖານ, ແລະພິມຜົນໄດ້ຮັບຕາມມາດຕະຖານ.

ສໍາລັບການນໍາໃຊ້ batch-oriented ຂອງ Coq, ເບິ່ງ coqc(1).

OPTIONS

-ຊ, - ຊ່ວຍ
ຊ່ວຍເຫຼືອ. ຈະໃຫ້ທ່ານບັນຊີລາຍຊື່ຄົບຖ້ວນຂອງທາງເລືອກທີ່ຍອມຮັບໂດຍ coqtop.

-I ແມ່ນ, --ລວມ dir
ເພີ່ມໄດເລກະທໍລີ dir ຢູ່ໃນເສັ້ນທາງລວມ

-R dir coqdir
ແຜນທີ່ທາງກາຍຍະພາບ recursively dir ກັບເຫດຜົນ coqdir

-ທາງເທີງ coqdir
ຕັ້ງຊື່ລະດັບສູງສຸດເປັນ coqdir ແທນ Top

- ລັດ​ປ້ອນ​ຂໍ້​ມູນ​ ຊື່​ເອ​ກະ​ສານ, - ແມ່ນ ຊື່​ເອ​ກະ​ສານ
ອ່ານສະຖານະຈາກໄຟລ໌ filename.coq

- ສຽງດັງ ເລີ່ມຕົ້ນດ້ວຍສະຖານະເບື້ອງຕົ້ນຫວ່າງເປົ່າ

- outputstateຊື່​ເອ​ກະ​ສານ
ຂຽນສະຖານະໃນໄຟລ໌ filename.coq

-load-ml-object ຊື່​ເອ​ກະ​ສານ
ໂຫຼດໄຟລ໌ວັດຖຸ ML ຊື່ໄຟລ໌

-load-ml-ແຫຼ່ງ ຊື່​ເອ​ກະ​ສານ
ໂຫຼດໄຟລ໌ ML ຊື່​ເອ​ກະ​ສານ

-load-vernac-ແຫຼ່ງ ຊື່​ເອ​ກະ​ສານ, -l ຊື່​ເອ​ກະ​ສານ
ໂຫລດໄຟລ໌ Coq filename.v (ໂຫຼດຊື່ໄຟລ໌.)

-load-vernac-source-verbose ຊື່​ເອ​ກະ​ສານ, -lv ຊື່​ເອ​ກະ​ສານ
ໂຫລດໄຟລ໌ Coq verbosely filename.v (ໂຫຼດຊື່ໄຟລ໌ Verbose.)

-load-vernac-object ຊື່​ເອ​ກະ​ສານ
ໂຫລດໄຟລ໌ວັດຖຸ Coq filename.vo

- ຮຽກ​ຮ້ອງ​ໃຫ້​ມີ​ ຊື່​ເອ​ກະ​ສານ
ໂຫລດໄຟລ໌ວັດຖຸ Coq filename.vo ແລະ​ນໍາ​ເຂົ້າ​ມັນ (ຕ້ອງ​ການ​ນໍາ​ເຂົ້າ​ຊື່​ໄຟລ​໌​.​)

- ລວບລວມ ຊື່​ເອ​ກະ​ສານ
ລວບລວມໄຟລ໌ Coq filename.v (ໝາຍເຖິງ - ຊຸດ )

-compile-verbose ຊື່​ເອ​ກະ​ສານ
verbosely ລວບລວມໄຟລ໌ Coq filename.v (ໝາຍເຖິງ - ຊຸດ )

-ທາງເລືອກ ດໍາເນີນການສະບັບພາສາພື້ນເມືອງຂອງ Coq

-byte ດໍາເນີນການສະບັບ bytecode ຂອງ Coq

- ບ່ອນໃດ ພິມສະຖານທີ່ຫ້ອງສະຫມຸດມາດຕະຖານຂອງ Coq ແລະອອກ

-v ພິມສະບັບ Coq ແລະອອກ

-q ຂ້າມການໂຫຼດ rcfile

-init-file ຊື່​ເອ​ກະ​ສານ
ຕັ້ງ rcfile ເປັນ ຊື່​ເອ​ກະ​ສານ

- ຊຸດ ຮູບ​ແບບ batch (ອອກ​ພຽງ​ແຕ່​ຫຼັງ​ຈາກ​ການ​ວິ​ເຄາະ arguments​)

- ບູດ ໂໝດ boot (ໝາຍເຖິງ -q ແລະ - ຊຸດ )

-emacs ບອກ Coq ວ່າມັນຖືກປະຕິບັດພາຍໃຕ້ Emacs

- dump-glob ຊື່​ເອ​ກະ​ສານ
dump globalizations ໃນໄຟລ໌ f (ເພື່ອນໍາໃຊ້ໂດຍ coqdoc(1​) )

- ມີ Geoproof (ແມ່ນ|ບໍ່)
ເພື່ອ (de)ເປີດໃຊ້ຫນ້າທີ່ພິເສດສໍາລັບ Geoproof ພາຍໃນ Coqide (ຄ່າເລີ່ມຕົ້ນແມ່ນ yes )

- ຄາດ​ຄະ​ເນ​ຊຸດ​
set sort ກໍານົດ impredicative

-dont-load-proofs
ຢ່າໂຫຼດຫຼັກຖານສະແດງ opaque ໃນຫນ່ວຍຄວາມຈໍາ

-xml ສົ່ງອອກໄຟລ໌ XML ໄປຫາລໍາດັບຊັ້ນທີ່ຮາກຖານຢູ່ໃນໄດເລກະທໍລີ
$COQ_XML_LIBRARY_ROOT (ຖ້າຕັ້ງ) ຫຼືເພື່ອ stdout (ຖ້າບໍ່ໄດ້ຕັ້ງ)

ຄວາມເປັນໄປໄດ້
ປັບປຸງຄວາມຖືກຕ້ອງຂອງຂໍ້ກໍານົດຫຼັກຖານທີ່ຜະລິດໂດຍກົນລະຍຸດບາງຢ່າງ

ໃຊ້ coqtop ອອນໄລນ໌ໂດຍໃຊ້ບໍລິການ onworks.net