Ini adalah perintah coqchk yang dapat dijalankan di penyedia hosting gratis OnWorks menggunakan salah satu dari beberapa workstation online gratis kami seperti Ubuntu Online, Fedora Online, emulator online Windows atau emulator online MAC OS
PROGRAM:
NAMA
coqchk - Pemeriksa Pustaka Coq Proof Checker yang dikompilasi
RINGKASAN
coqchk [ Pilihan ] modul
DESKRIPSI
coqchk adalah pemeriksa mandiri dari pustaka yang dikompilasi (file .vo diproduksi oleh coqc) untuk
Asisten Bukti Coq. Lihat Manual Referensi untuk informasi lebih lanjut. Ia kembali dengan
keluar kode 0 jika semua tugas yang diminta berhasil. Kode pengembalian bukan nol berarti bahwa
ada yang salah: beberapa perpustakaan tidak ditemukan, konten rusak, pemeriksaan jenis
kegagalan, dll.
modul adalah daftar modul yang akan diperiksa. Modul dapat disebut dengan singkatan atau
nama yang memenuhi syarat.
PILIHAN
-I aku s, --termasuk dir
tambahkan direktori dir di jalur sertakan
-R dir coqdir
memetakan fisik secara rekursif dir untuk logis coqdir
-diam
membuat coqchk kurang bertele-tele.
-mengakui modul
beri tag modul yang ditentukan dan semua dependensinya sebagai tepercaya, dan tidak akan
diperiksa ulang, kecuali jika diminta secara eksplisit oleh opsi lain.
-norec modul
menentukan bahwa modul yang diberikan harus diverifikasi tanpa meminta untuk memeriksanya
ketergantungan.
-M, --Penyimpanan
menampilkan ringkasan memori yang digunakan oleh pemeriksa.
-Hai, --output-konteks
menampilkan ringkasan konten logis yang telah diverifikasi: asumsi dan
penggunaan impredikatif.
-impredikatif-set
memungkinkan pemeriksa menerima pustaka yang telah dikompilasi dengan flag ini.
-v cetak versi coqchk dan keluar.
-coqlib dir
menimpa lokasi default perpustakaan standar.
-di mana cetak lokasi perpustakaan standar coqchk dan keluar.
-H, --membantu
cetak daftar opsi
Gunakan coqchk online menggunakan layanan onworks.net
