coqdoc - Online w chmurze

PROGRAM:

IMIĘ

coqdoc — narzędzie dokumentacyjne dla asystenta Coq proof

STRESZCZENIE

koqdoc [ Opcje ] pliki

OPIS

koqdoc to narzędzie dokumentacyjne dla asystenta Coq proof. Tworzy LaTeX lub HTML
dokumentów z zestawu plików Coq. Zobacz dokumentację referencyjną Coq (url
poniżej).

OPCJE

Ogólnie Opcje
-h Pomoc. Poda pełną listę opcji akceptowanych przez coqdoc.

--html Wybierz wyjście HTML.

--lateks
Wybierz wyjście LATEX.

--dvi Wybierz wyjście DVI.

--ps Wybierz wydruk PostScript.

--texmacs
Wybierz wyjście TeXmacsa.

-- stdout
Przekieruj wyjście na stdout

-o file,--wyjście filet
Przekieruj dane wyjściowe do pliku plik.

-d reż, --informator reż
Pliki wyjściowe do katalogu reż zamiast bieżącego katalogu (opcja -d nie
zmień nazwę pliku określoną opcją -o, jeśli istnieje).

-tak, --niski
Nie wstawiaj tytułów plików. Domyślnym zachowaniem jest wstawienie tytułu takiego jak
``Library Foo'' dla każdego pliku.

-t strunowy, --tytuł ciąg
Ustaw tytuł dokumentu.

--tylko ciało
Pomiń nagłówek i zakończenie dokumentu końcowego. W ten sposób można wstawić
wynikowy dokument w większy.

-p strunowy, --preambuła ciąg
Wstaw trochę materiału do preambuły LATEX-a, tuż przed \begin{document}
(bez znaczenia z -html).

--vernac-plik file, --tex-plik filet
Traktuje plik `file' odpowiednio jako plik .v (lub .g) lub plik .tex.

--pliki-z filet
Czytaj nazwy plików do przetworzenia w pliku `file' tak, jakby były podane w poleceniu
linia. Przydatne w przypadku źródeł programu podzielonych na kilka katalogów.

-Q, --cichy
Bądź cicho. Nie drukuj niczego poza błędami.

-H, --help
Podaj krótkie podsumowanie opcji i wyjdź.

-v, --wersja
Wydrukuj wersję i wyjdź.

wskaźnik Opcje
Domyślnym zachowaniem jest budowanie indeksu, tylko dla danych wyjściowych HTML, w pliku index.html.

--bez indeksu
Nie wysyłaj indeksu.

--wiele indeksów
Wygeneruj jedną stronę dla każdej kategorii i każdej litery w indeksie wraz z a
górna strona index.html.

Stół of treść opcja
-toc, --spis-treści
Wstaw spis treści. Dla wyjścia LATEX wstawia \tableofcontents at
początek dokumentu. W przypadku wyjścia HTML tworzy spis treści
do toc.html.

Hiperłącza Opcje
--glob-z filet
Twórz odniesienia za pomocą globalizacji Coq z pliku plik. (Takie globalizacje są
uzyskany z opcją Coq -dump-glob).

--no-zewnętrzne
Nie wstawiaj linków do standardowej biblioteki Coq.

--zewnętrzny url biblioteka
Ustaw podstawowy adres URL dla biblioteki zewnętrznej, której prefiks katalogu głównego to libroot.

--coqlib url
Ustaw podstawowy adres URL dla standardowej biblioteki Coq (domyślnie to
http://coq.inria.fr/library/).

--coqlib_ścieżka reż
Ustaw ścieżkę podstawową, w której są instalowane pliki Coq, zwłaszcza pliki stylów
coqdoc.sty i coqdoc.css.

-R reż koqdir
Odwzoruj katalog fizyczny dir na katalog logiczny Coq coqdir (podobnie jak opcja Coq
-R). Uwaga: opcja -R ma wpływ tylko na pliki następujące po niej w poleceniu
line, więc prawdopodobnie będziesz musiał najpierw ustawić tę opcję.

Spis treści Opcje
-G, --gallina
Nie drukuj odbitek próbnych.

-ja, --światło
Tryb światła. Pomiń dowody (jak w przypadku -g) i następujące polecenia:

* [Rekurencyjna] Definicja taktyki
* Podpowiedź / Wskazówki
* Wymagać
* Przezroczysty / Nieprzezroczysty
* Niejawny argument / implikacje
* Sekcja / Zmienna / Hipoteza / Koniec

Zachowanie opcji -g i -l można lokalnie przesłonić za pomocą (* begin show
*) ... (* koniec pokazu *) środowisko (patrz wyżej).

Wybierz język Opcje
Domyślnym zachowaniem jest przyjmowanie 7-bitowych plików wejściowych ASCII.

-łac.1, --łac.1
Wybierz pliki wejściowe ISO-8859-1. Jest odpowiednikiem --inputenc latin1 --charset
iso-8859-1.

-utf8, --utf8
Wybierz pliki wejściowe UTF-8 (Unicode). Jest odpowiednikiem --inputenc utf8 --charset
utf-8. Wsparcie dla LATEX UTF-8 można znaleźć pod adresem
http://www.ctan.org/tex-archive/macros/latex/contrib/supported/unicode/.

--wejście ciąg
Podaj kodowanie wejścia LATEX jako opcję do pakietu LATEX inputenc.

--zestaw znaków ciąg
Określ zestaw znaków HTML, który ma zostać wstawiony w nagłówku HTML.

Korzystaj z coqdoc online, korzystając z usług onworks.net