coqdoc - Bulutta Çevrimiçi

Program:

ADI

coqdoc - Coq kanıt yardımcısı için bir belgeleme aracı

SİNOPSİS

coqdoc [ seçenekleri ] Dosyaları

TANIM

coqdoc Coq kanıt asistanı için bir dokümantasyon aracıdır. LaTeX veya HTML oluşturur
bir dizi Coq dosyasından belgeler. Belgeler için Coq referans kılavuzuna bakın (url
altında).

SEÇENEKLER

Genel seçenekleri
-h Yardım. coqdoc tarafından kabul edilen seçeneklerin tam listesini verecektir.

--html Bir HTML çıktısı seçin.

--lateks
Bir LATEX çıktısı seçin.

--dvi Bir DVI çıkışı seçin.

--ps Bir PostScript çıktısı seçin.

--texmac'ler
Bir TeXmacs çıktısı seçin.

--stdout
Çıktıyı stdout'a yönlendir

-o dosyası,--çıktı dosya
Çıktıyı dosyaya yönlendir dosyası.

-d dir --dizin dir
Dosyaları dizine çıkar dir geçerli dizin yerine (seçenek -d
varsa -o seçeneğiyle belirtilen dosya adını değiştirin).

-Evet, --kısa boylu
Dosyalar için başlık eklemeyin. Varsayılan davranış, şöyle bir başlık eklemektir
Her dosya için ``Library Foo''.

-t dize, --Başlık dizi
Belge başlığını ayarlayın.

--sadece vücut
Nihai belgenin başlığını ve fragmanını gizleyin. Böylece, ekleyebilirsiniz
elde edilen belgeyi daha büyük bir belgeye dönüştürür.

-p dize, --önsöz dizi
\begin{belge}'den hemen önce LATEX girişine biraz malzeme ekleyin
(-html ile anlamsız).

--vernac dosyası dosyası, --tex dosyası dosya
Dosyayı sırasıyla bir .v (veya .g) dosyası veya bir .tex dosyası olarak kabul eder.

--dosyalar-dan dosya
Dosya adlarını komutta verilmiş gibi "dosya" dosyasında işlenecek dosya adlarını okuyun
hat. Birkaç dizine bölünmüş program kaynakları için kullanışlıdır.

-Q, --sessizlik
Sessiz olun. Hatalar dışında hiçbir şey yazdırmayın.

-H, --yardım et
Seçeneklerin kısa bir özetini verin ve çıkın.

-içinde, --versiyon
Sürümü yazdırın ve çıkın.

indeks seçenekleri
Varsayılan davranış, yalnızca HTML çıktısı için index.html'de bir dizin oluşturmaktır.

--no-indeks
İndeks çıktısı vermeyin.

--çoklu dizin
Her kategori ve dizindeki her harf için bir sayfa oluşturun.
üst sayfa index.html.

tablo of içindekiler seçenek
-tc, --içindekiler
İçindekiler tablosu ekleyin. Bir LATEX çıktısı için, şu adrese bir \tableofcontents ekler.
belgenin başlangıcı. Bir HTML çıktısı için bir içindekiler tablosu oluşturur
toc.html içine.

Köprüler seçenekleri
--glob-dan dosya
Dosya dosyasından Coq küreselleştirmelerini kullanarak referanslar yapın. (Bu tür küreselleşmeler
Coq seçeneği -dump-glob ile elde edilir).

--hiçbir-harici
Coq standart kitaplığına bağlantılar eklemeyin.

--harici url kök kök
Kök öneki libroot olan harici kitaplık için temel URL'yi ayarlayın.

--coqlib url
Coq standart kitaplığı için temel URL'yi ayarlayın (varsayılan
http://coq.inria.fr/library/).

--coqlib_path dir
Coq dosyalarının, özellikle stil dosyalarının yüklendiği temel yolu ayarlayın
coqdoc.sty ve coqdoc.css.

-R dir kokdir
Fiziksel dizin dizinini Coq mantıksal dizini coqdir ile eşleyin (Coq seçeneğine benzer şekilde
-R). Not: -R seçeneği, yalnızca komutta onu izleyen dosyalar üzerinde etkilidir
satırı, bu yüzden muhtemelen önce bu seçeneği koymanız gerekecek.

İçerik seçenekleri
-G, --gallina
Kanıtları yazdırmayın.

-ben, --ışık
Işık modu. Kanıtları (-g ile olduğu gibi) ve aşağıdaki komutları bastırın:

* [Yinelemeli] Taktik Tanımı
* İpucu / İpuçları
* Gerekmek
* Şeffaf / Opak
* Örtük Argüman / Örtükler
* Bölüm / Değişken / Hipotez / Son

-g ve -l seçeneklerinin davranışı, (* start show kullanılarak yerel olarak geçersiz kılınabilir.
*) ... (* bitiş gösterisi *) ortam (yukarıya bakın).

Dil seçenekleri
Varsayılan davranış, ASCII 7 bit giriş dosyalarını varsaymaktır.

-latince1, --latin1
ISO-8859-1 girdi dosyalarını seçin. --inputenc latin1 --charset ile eşdeğerdir
iso-8859-1.

-utf8, --utf8
UTF-8 (Unicode) giriş dosyalarını seçin. --inputenc utf8 --charset ile eşdeğerdir
utf-8. LATEX UTF-8 desteği şu adreste bulunabilir:
http://www.ctan.org/tex-archive/macros/latex/contrib/supported/unicode/.

--giriş dizi
LATEX paket girdisine bir seçenek olarak bir LATEX girdi kodlaması verin.

--karakter seti dizi
HTML başlığına eklenecek HTML karakter kümesini belirtin.

onworks.net hizmetlerini kullanarak coqdoc'u çevrimiçi kullanın