coqdoc - онлайн у хмарі

ПРОГРАМА:

ІМ'Я

coqdoc - інструмент документації для Coq proof Assistant

СИНТАКСИС

coqdoc [ опції ] файли

ОПИС

coqdoc є інструментом документації для Coq proof Assistant. Він створює LaTeX або HTML
документи з набору файлів Coq. Перегляньте довідковий посібник Coq для отримання документації (url
нижче).

ВАРІАНТИ

Загальний опції
-h Допоможіть. Надасть вам повний список опцій, прийнятих coqdoc.

--html Виберіть вихідний HTML-код.

--латекс
Виберіть вихід LATEX.

--dvi Виберіть вихід DVI.

--ps Виберіть вихід PostScript.

--texmacs
Виберіть вихід TeXmacs.

--stdout
Перенаправити вихід на стандартний вихід

-o файл,- вихід файл
Переспрямуйте вихід у файл файлу.

-d реж., --каталог реж
Вивести файли в каталог реж замість поточного каталогу (опція -d не робить
змінити ім’я файлу, зазначене опцією -o, якщо є).

-так, --короткі
Не вставляйте заголовки для файлів. Поведінка за замовчуванням – вставляти заголовок, як
``Бібліотека Foo'' для кожного файлу.

-t струна, -- назва рядок
Встановіть назву документа.

--лише тіло
Придушити заголовок і кінцевий текст остаточного документа. Таким чином, ви можете вставити
отриманий документ у більший.

-p струна, -- преамбула рядок
Вставте деякий матеріал у преамбулу LATEX безпосередньо перед \begin{document}
(безглуздо з -html).

--vernac-файл файл, --tex-файл файл
Розглядає файл `file' відповідно як файл .v (або .g) або файл .tex.

--файли-від файл
Прочитайте імена файлів для обробки у файлі `file' так, ніби вони були дані командою
лінія. Корисно для програмних джерел, розділених на кілька каталогів.

-q, --спокійно
Тихо. Не друкуйте нічого, крім помилок.

-h, --допомога
Дайте короткий підсумок варіантів і вийдіть.

-v, -- версія
Роздрукуйте версію та вийдіть.

індекс опції
Поведінка за замовчуванням полягає у створенні індексу, лише для виведення HTML, у index.html.

--без індексу
Не виводьте індекс.

--багатоіндексний
Створіть одну сторінку для кожної категорії та кожної літери в індексі разом із a
верхня сторінка index.html.

таблиця of зміст варіант
-toc, --зміст
Вставте зміст. Для виводу LATEX він вставляє \tableofcontents at
початок документа. Для виводу HTML він створює таблицю змісту
в toc.html.

Гіперпосилання опції
--glob-від файл
Зробіть посилання за допомогою глобалізації Coq з файлу. (Такі глобалізації є
отримано з опцією Coq -dump-glob).

--без зовнішніх
Не вставляйте посилання на стандартну бібліотеку Coq.

--зовнішні URL libroot
Встановити базову URL-адресу для зовнішньої бібліотеки, кореневим префіксом якої є libroot.

--coqlib URL
Встановити базову URL-адресу для стандартної бібліотеки Coq (за замовчуванням
http://coq.inria.fr/library/).

--coqlib_шлях реж
Встановіть базовий шлях, куди встановлюються файли Coq, особливо файли стилів
coqdoc.sty і coqdoc.css.

-R реж coqdir
Зіставте фізичний каталог dir на логічний каталог Coq coqdir (подібно до параметра Coq
-R). Примітка: Параметр -R впливає лише на наступні за ним файли за командою
рядок, тож вам, ймовірно, доведеться поставити цей параметр першим.

зміст опції
-g, --галлина
Не друкуйте проби.

-л, --світло
Світлий режим. Придушити докази (як з -g) і такі команди:

* [Рекурсивне] Визначення тактики
* Підказка / Підказки
* Вимагати
* Прозорий / непрозорий
* Неявний аргумент / Неявний
* Розділ / Змінна / Гіпотеза / Кінець

Поведінку параметрів -g та -l можна локально змінити за допомогою (* begin show
*) ... (* закінчення шоу *) середовище (див. вище).

Language опції
Поведінка за замовчуванням передбачає 7-бітові вхідні файли ASCII.

-латиниця1, --латиниця1
Виберіть вхідні файли ISO-8859-1. Це еквівалентно --inputenc latin1 --charset
iso-8859-1.

-utf8, --utf8
Виберіть вхідні файли UTF-8 (Unicode). Це еквівалентно --inputenc utf8 --charset
utf-8. Підтримку LATEX UTF-8 можна знайти за адресою
http://www.ctan.org/tex-archive/macros/latex/contrib/supported/unicode/.

--inputenc рядок
Надайте кодування введення LATEX, як опцію пакету LATEX inputenc.

--набір символів рядок
Вкажіть набір символів HTML, який потрібно вставити в заголовок HTML.

Використовуйте coqdoc онлайн за допомогою служб onworks.net