Ini adalah perintah coqmktop 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
coqmktop - Tautan taktik pengguna Coq Proof Assistant
RINGKASAN
coqmktop [ Pilihan ] arsip
DESKRIPSI
coqmktop membangun tingkat atas Coq baru yang diperluas dengan taktik pengguna. arsip adalah Tujuan
Objek Caml atau file perpustakaan (yaitu dengan akhiran .cmo, .cmx, .cma atau .cmxa) untuk ditautkan dengan
sistem coq. Linker menghasilkan toplevel Coq yang dapat dieksekusi yang dapat dipanggil secara langsung
Atau melalui coqc(1), menggunakan opsi -gambar.
PILIHAN
-h Membantu. Daftar opsi yang tersedia.
-srcdir dir
Tentukan di mana file sumber Coq berada
-o file-exe
Tentukan nama toplevel yang dihasilkan
-memilih Kompilasi dalam kode asli
-penuh Tautkan taktik tingkat tinggi
-puncak Bangun Coq di tingkat atas ocaml (tidak kompatibel dengan -memilih)
-R dir Tentukan direktori secara rekursif untuk Ocaml
-v8 Tautan dengan tata bahasa V8
Gunakan coqmktop online menggunakan layanan onworks.net