Ini ialah arahan coqmktop 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
coqmktop - Penyambung taktik pengguna Coq Proof Assistant
SINOPSIS
coqmktop [ pilihan ] fail
DESCRIPTION
coqmktop membina peringkat teratas Coq baharu yang dilanjutkan dengan taktik pengguna. fail adalah Objektif
Fail objek atau perpustakaan Caml (iaitu dengan akhiran .cmo, .cmx, .cma atau .cmxa) untuk dipautkan dengan
Sistem Coq. Penyambung menghasilkan peringkat atas Coq boleh laku yang boleh dipanggil terus
atau melalui coqc(1), menggunakan pilihan -image.
PILIHAN
-h Tolong. Senaraikan pilihan yang ada.
-srcdir dir
Nyatakan di mana fail sumber Coq berada
-o fail exec
Nyatakan nama peringkat atas yang terhasil
-pilih Susun dalam kod asli
-penuh Pautkan taktik peringkat tinggi
-atas Bina Coq pada tingkat atas ocaml (tidak serasi dengan -pilih)
-R dir Tentukan direktori rekursif untuk Ocaml
-v8 Pautan dengan tatabahasa V8
Gunakan coqmktop dalam talian menggunakan perkhidmatan onworks.net
