CoqのソースコードをカッコイイHTMLページにする方法(coqdocを使う)
Coqでプログラムや証明を書いたら、そのソースコードを人に見せたりしたくなるときがある。
そのときに便利なcoqdocという機能がある。coqdocはcoqtopやcoqcなどと一緒のところにある。
使いかたは以下。
$ coqdoc [Coqファイル.v]
ここで、(** コメント *)のように星二つで作ったコメントはドキュメントに青く出力される。特に大きい見出しとして出力したい場合は(** * 見出し *)というコメントにしよう。
コメント内でリンクタグなどのHTMLを書きたい場合は#で囲ったら大丈夫。
さらにスタンダードライブラリなど、どの関数や定理を使ったかリンクがたどれるドキュメントを作ることもできる。それには次のようなオプションつきで、コンパイルしなおしてからcoqdocするとできる。
$ coqc -dump-glob [新たに生成されるglobファイル] [Coqファイル.v] $ coqdoc --glob-from [生成されたglobファイル] [Coqファイル.v]
ドキュメント生成後にCoqファイルを編集した場合は、globファイルを削除してからやり直す必要があることに注意しよう。
日本語などを使いたい場合はutf-8エンコーディングにして、coqdocの際に--utf8オプションをつけよう。
また、--latexオプションでTeXのファイルを出力することもできる。
次は簡単な例とそれを生成したときのコマンドである。
$ coqc -dump-glob coqdoc_example.glob coqdoc_example.v $ coqdoc -utf8 --glob-from coqdoc_example.glob coqdoc_example.v
