Ini ialah arahan coqchk yang boleh dijalankan dalam penyedia pengehosan percuma OnWorks menggunakan salah satu daripada berbilang stesen kerja dalam talian percuma kami seperti Ubuntu Online, Fedora Online, emulator dalam talian Windows atau emulator dalam talian MAC OS.
JADUAL:
NAMA
coqchk - Pemeriksa Bukti Coq menyusun pengesah perpustakaan
SINOPSIS
coqchk [ pilihan ] modul
DESCRIPTION
coqchk ialah penyemak kendiri perpustakaan yang disusun (fail.vo yang dihasilkan oleh coqc) untuk
Pembantu Bukti Coq. Lihat Manual Rujukan untuk maklumat lanjut. Ia kembali dengan
keluar kod 0 jika semua tugas yang diminta berjaya. Kod pulangan bukan sifar bermakna itu
sesuatu telah berlaku: beberapa perpustakaan tidak ditemui, kandungan rosak, semakan jenis
kegagalan, dsb.
modul ialah senarai modul yang perlu disemak. Modul boleh dirujuk dengan pendek atau
nama yang layak.
PILIHAN
-I adalah, --termasuk dir
tambah direktori dir dalam laluan termasuk
-R dir coqdir
memetakan fizikal secara rekursif dir kepada logik coqdir
-senyap
menjadikan coqchk kurang bertele-tele.
-mengaku modul
tag modul yang ditentukan dan semua kebergantungannya sebagai dipercayai, dan tidak akan
disemak semula, melainkan diminta secara eksplisit oleh pilihan lain.
-norec modul
menyatakan bahawa modul yang diberikan hendaklah disahkan tanpa meminta untuk menyemaknya
kebergantungan.
-m, --ingatan
memaparkan ringkasan memori yang digunakan oleh penyemak.
-o, --output-context
memaparkan ringkasan kandungan logik yang telah disahkan: andaian dan
penggunaan impredikativiti.
-impredicative-set
membenarkan penyemak untuk menerima perpustakaan yang telah disusun dengan bendera ini.
-v cetak versi coqchk dan keluar.
-coqlib dir
mengatasi lokasi lalai perpustakaan standard.
-di mana cetak lokasi perpustakaan standard coqchk dan keluar.
-h, - membantu
cetak senarai pilihan
Gunakan coqchk dalam talian menggunakan perkhidmatan onworks.net
