coqdoc - クラウド上のオンライン

プログラム：

NAME

coqdoc - Coq 証明アシスタント用のドキュメント ツール

SYNOPSIS

コクドック [ オプション ] ファイル

DESCRIPTION

コクドック は、Coq 証明アシスタント用のドキュメント ツールです。 LaTeX または HTML を作成します
一連の Coq ファイルからのドキュメント。 ドキュメントについては、Coq リファレンス マニュアルを参照してください (URL
下）。

OPTIONS

全体 オプション
-h ヘルプ。 coqdoc で受け入れられるオプションの完全なリストが表示されます。

--html HTML 出力を選択します。

- ラテックス
LATEX 出力を選択します。

--dvi DVI 出力を選択します。

--ps PostScript 出力を選択します。

--texmacs
TeXmacs 出力を選択します。

--stdout
出力を標準出力にリダイレクトします

-o ファイル、- 出力 file
出力をファイルにリダイレクトします ファイルにソフトウェアを指定する必要があります。

-d 監督、 - ディレクトリ DIR
ファイルをディレクトリに出力する DIR 現在のディレクトリの代わりに (オプション -d はそうではありません)
オプション -o で指定されたファイル名があれば変更します)。

-s、 - 短い
ファイルにタイトルを挿入しないでください。 デフォルトの動作では、次のようなタイトルが挿入されます。
ファイルごとに「Library Foo」。

-t ひも、 - 題名 文字列
文書のタイトルを設定します。

--本体のみ
最終ドキュメントのヘッダーとトレーラーを非表示にします。 したがって、次のように挿入できます。
結果のドキュメントをより大きなドキュメントに変換します。

-p ひも、 - 前文 文字列
LATEX プリアンブルの \begin{document} の直前にマテリアルを挿入します。
(-html では意味がありません)。

--vernac-ファイル ファイル、 --tex-ファイル file
ファイル「file」をそれぞれ .v (または .g) ファイルまたは .tex ファイルとみなします。

--files-from file
コマンドで指定されたかのように、ファイル `file' 内で処理するファイル名を読み取ります。
ライン。 プログラム ソースが複数のディレクトリに分割されている場合に便利です。

-NS、 - 静かな
静かに。 エラー以外は何も出力しません。

-NS、 - 助けて
オプションの短い概要を入力して終了します。

-v、 - バージョン
バージョンを印刷して終了します。

インデックス オプション
デフォルトの動作では、HTML 出力のみのインデックスをindex.html に構築します。

-インデックスなし
インデックスを出力しません。

--マルチインデックス
各カテゴリーおよび索引内の各文字に対して XNUMX ページを生成し、
トップページindex.html。

表 of 中身 オプション
-toc、 - 目次
目次を挿入します。 LATEX 出力の場合、\tableofcontents を次の位置に挿入します。
文書の冒頭。 HTML 出力の場合、目次を作成します。
toc.html にコピーします。

ハイパーリンク オプション
--glob-from file
ファイル file から Coq グローバリゼーションを使用して参照を作成します。 （このようなグローバリゼーションは、
Coq オプション -dump-glob で取得)。

--外部なし
Coq 標準ライブラリへのリンクを挿入しないでください。

- 外部の URL リブルート
ルートプレフィックスが libroot である外部ライブラリのベース URL を設定します。

--coqlib URL
Coq 標準ライブラリのベース URL を設定します (デフォルトは
http://coq.inria.fr/library/).

--coqlib_path DIR
Coq ファイル、特にスタイル ファイルがインストールされるベース パスを設定します。
coqdoc.sty と coqdoc.css。

-R DIR コクディル
物理ディレクトリ dir を Coq 論理ディレクトリ coqdir にマップします (Coq オプションと同様)
-R）。 注： オプション -R は、コマンドでそれに続くファイルにのみ影響します。
したがって、おそらくこのオプションを最初に置く必要があります。

内容 オプション
-NS、 --ガリーナ
校正刷りは印刷しないでください。

-l、 - ライト
ライトモード。 プルーフ (-g と同様) と次のコマンドを抑制します。

* [再帰的] 戦術定義
*ヒント/ヒント
* 必須
* 透明/不透明
* 暗黙的な引数/暗黙的
* セクション / 変数 / 仮説 / 終了

オプション -g および -l の動作は、(* begin show
*) ... (* ショー終了 *) 環境 (上記を参照)。

言語設定 オプション
デフォルトの動作では、ASCII 7 ビット入力ファイルが想定されます。

-ラテン1、 --latin1
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 パッケージ inputenc のオプションとして、LATEX 入力エンコーディングを指定します。

- 文字コード 文字列
HTML ヘッダーに挿入される HTML 文字セットを指定します。

onworks.net サービスを使用してオンラインで coqdoc を使用する