Ini ialah arahan coqdoc 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
coqdoc - Alat dokumentasi untuk pembantu kalis Coq
SINOPSIS
coqdoc [ pilihan ] fail
DESCRIPTION
coqdoc ialah alat dokumentasi untuk pembantu kalis Coq. Ia mencipta LaTeX atau HTML
dokumen daripada set fail Coq. Lihat manual rujukan Coq untuk dokumentasi (url
di bawah).
PILIHAN
Keseluruhan pilihan
-h Tolong. Akan memberikan anda senarai lengkap pilihan yang diterima oleh coqdoc.
--html Pilih output HTML.
--lateks
Pilih output LATEX.
--dvi Pilih output DVI.
--ps Pilih output PostScript.
--texmacs
Pilih output TeXmacs.
--stdout
Ubah hala output ke stdout
-o fail,--pengeluaran fail
Ubah hala output ke dalam fail fail.
-d adalah, --direktori dir
Keluarkan fail ke dalam direktori dir bukannya direktori semasa (pilihan -d tidak
tukar nama fail yang ditentukan dengan pilihan -o, jika ada).
-ya, --pendek
Jangan masukkan tajuk untuk fail. Tingkah laku lalai adalah untuk memasukkan tajuk seperti
``Library Foo'' untuk setiap fail.
-t tali, --tajuk rentetan
Tetapkan tajuk dokumen.
--badan-sahaja
Sekat pengepala dan treler dokumen akhir. Oleh itu, anda boleh memasukkan
menghasilkan dokumen menjadi lebih besar.
-p tali, --mukadimah rentetan
Masukkan beberapa bahan dalam mukadimah LATEX, betul-betul sebelum \begin{document}
(tidak bermakna dengan -html).
--vernac-file fail, --tex-file fail
Pertimbangkan fail `fail' masing-masing sebagai fail .v (atau .g) atau fail .tex.
--fail-daripada fail
Baca nama fail untuk diproses dalam fail `fail' seolah-olah ia diberikan pada arahan
barisan. Berguna untuk sumber program berpecah dalam beberapa direktori.
-q, --senyap
Senyap. Jangan cetak apa-apa kecuali ralat.
-h, - membantu
Berikan ringkasan ringkas tentang pilihan dan keluar.
-v, --versi
Cetak versi dan keluar.
indeks pilihan
Tingkah laku lalai adalah untuk membina indeks, untuk output HTML sahaja, ke dalam index.html.
--tiada-indeks
Jangan keluarkan indeks.
--berbilang indeks
Hasilkan satu halaman untuk setiap kategori dan setiap huruf dalam indeks, bersama-sama dengan a
halaman atas index.html.
Jadual of kandungan pilihan
-toc, --isi kandungan
Masukkan jadual kandungan. Untuk keluaran LATEX, ia memasukkan \tableofcontents at
permulaan dokumen. Untuk output HTML, ia membina jadual kandungan
ke dalam toc.html.
Hyperangkai pilihan
--glob-daripada fail
Buat rujukan menggunakan globalisasi Coq daripada fail fail. (Globalisasi tersebut adalah
diperoleh dengan pilihan Coq -dump-glob).
--tiada-luaran
Jangan masukkan pautan ke perpustakaan standard Coq.
--luaran url buku
Tetapkan URL asas untuk pustaka luaran yang awalan akarnya ialah libroot.
--coqlib url
Tetapkan URL asas untuk pustaka standard Coq (lalai ialah
http://coq.inria.fr/library/).
--coqlib_path dir
Tetapkan laluan asas tempat fail Coq dipasang, terutamanya fail gaya
coqdoc.sty dan coqdoc.css.
-R dir coqdir
Petakan dir direktori fizikal ke direktori logik Coq coqdir (begitu juga dengan pilihan Coq
-R). Catatan: pilihan -R hanya mempunyai kesan pada fail yang mengikutinya pada arahan
baris, jadi anda mungkin perlu meletakkan pilihan ini dahulu.
Contents [show] pilihan
-g, --gallina
Jangan cetak bukti.
-l, --cahaya
Mod cahaya. Sekat bukti (seperti -g) dan arahan berikut:
* [Rekursif] Takrif Taktik
* Petunjuk / Petunjuk
* Memerlukan
* Telus / Legap
* Hujah Tersirat / Tersirat
* Bahagian / Pembolehubah / Hipotesis / Tamat
Tingkah laku pilihan -g dan -l boleh ditindih secara setempat menggunakan (* mulakan rancangan
*) ... (* tamat rancangan *) persekitaran (lihat di atas).
Bahasa pilihan
Tingkah laku lalai adalah untuk menganggap fail input ASCII 7 bit.
-latin1, --latin1
Pilih fail input ISO-8859-1. Ia bersamaan dengan --inputenc latin1 --charset
iso-8859-1.
-utf8, --utf8
Pilih fail input UTF-8 (Unicode). Ia bersamaan dengan --inputenc utf8 --charset
utf-8. Sokongan LATEX UTF-8 boleh didapati di
http://www.ctan.org/tex-archive/macros/latex/contrib/supported/unicode/.
--inputenc rentetan
Berikan pengekodan input LATEX, sebagai pilihan untuk inputenc pakej LATEX.
--charset rentetan
Tentukan set aksara HTML, untuk disisipkan dalam pengepala HTML.
Gunakan coqdoc dalam talian menggunakan perkhidmatan onworks.net