coqdoc - Интернет в облаке

ПРОГРАММА:

ИМЯ

coqdoc - инструмент для документирования помощника по проверке Coq.

СИНТАКСИС

кокдок [ кредита ] файлов

ОПИСАНИЕ

кокдок - это инструмент для документирования помощника по проверке Coq. Создает LaTeX или HTML
документы из набора файлов Coq. См. Справочное руководство Coq для документации (url
ниже).

ДОПОЛНИТЕЛЬНЫЕ УСЛУГИ, НЕ ВКЛЮЧЕННЫЕ В ПАКЕТ

В общем кредита
-h Помощь. Предоставит вам полный список вариантов, принятых coqdoc.

--html Выберите вывод HTML.

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

--dvi Выберите выход DVI.

--пс Выберите вывод PostScript.

--texmacs
Выберите выход TeXmacs.

--stdout
Перенаправить вывод на стандартный вывод

-o файл,--выход файл
Перенаправить вывод в файл .

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

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

-t строка, --заглавие string
Задайте заголовок документа.

- только тело
Скрыть заголовок и трейлер окончательного документа. Таким образом, вы можете вставить
получившийся документ в более крупный.

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

--vernac-файл файл, --tex-файл файл
Считает файл "файлом" соответственно файлом .v (или .g) или файлом .tex.

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

-д, --тихий
Будь спокоен. Не печатайте ничего, кроме ошибок.

-час, --Помогите
Кратко опишите варианты и выйдите.

-в, --версия
Распечатайте версию и выйдите.

Индекс кредита
По умолчанию индекс создается только для вывода HTML в index.html.

--без индекса
Не выводить индекс.

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

Настольные of содержание вариант
-ток, --оглавление
Вставьте оглавление. Для вывода LATEX он вставляет \ tableofcontents в
начало документа. Для вывода HTML он создает оглавление.
в toc.html.

Гиперссылки кредита
--glob-от файл
Делайте ссылки с помощью глобализации Coq из файлового файла. (Такие глобализации
получается с помощью опции Coq -dump-glob).

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

--внешний URL libroot
Установите базовый URL-адрес для внешней библиотеки, корневой префикс которой - libroot.

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

--coqlib_path директория
Задайте базовый путь, по которому устанавливаются файлы Coq, особенно файлы стилей
coqdoc.sty и coqdoc.css.

-R директория Coqdir
Сопоставить каталог физического каталога с логическим каталогом Coq coqdir (аналогично параметру Coq
-Р). Примечание: опция -R влияет только на файлы, следующие за ней в команде
строка, поэтому вам, вероятно, нужно будет сначала поставить эту опцию.

Содержание: кредита
-грамм, --галлина
Не печатайте пробные отпечатки.

-л, --свет
Легкий режим. Подавить доказательства (как с -g) и следующие команды:

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

Поведение опций -g и -l можно локально переопределить с помощью (* begin show
*) ... (* end show *) среда (см. выше).

Язык кредита
По умолчанию предполагается, что входные файлы ASCII 7 бит.

-латиница1, --latin1
Выберите входные файлы ISO-8859-1. Эквивалентно --inputenc latin1 --charset
изо-8859-1.

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

--inputenc string
Укажите входную кодировку LATEX в качестве опции для пакета LATEX inputenc.

--charset string
Укажите набор символов HTML, который будет вставлен в заголовок HTML.

Используйте coqdoc онлайн с помощью сервисов onworks.net