Coqのドキュメント生成ツールであるcoqdocはコマンドラインオプションによってHTML形式やPDF形式の書類を生成するが、PDF形式の書類を作成する際に内部でpdfTeXを使っているようで、日本語を含むソースコードを扱う場合は簡単にはうまくいかないことがある。
そこで、coqdocからはtex形式のファイルを出すところまでやってもらい、残りはplatexなど自分の好きな方法で処理したい。
次のような内容のMakeというファイルを追加すればわりと簡単に実現できる(CoqのソースコードはHoge.v, Piyo.vだとする)。
-R src JapaneseCoqdocSampleProject
src/Hoge.v
src/Piyo.v
-custom "platex Proof.tex; platex Proof.tex" "Proof.tex $(VOFILES) $(VFILES:.v=.tex)" "Proof.dvi"
-custom "dvipdfmx Proof.dvi" "Proof.dvi" Proof.pdf
また、プリアンブルなどに相当する部分Proof.texは自分で用意する。例えば次のような感じ。
\documentclass[12pt]{jreport}
\usepackage[]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{fullpage}
\usepackage{coqdoc}
\usepackage{amsmath,amssymb}
\begin{document}
\title{証明報告書}
\author{有限会社 ITプランニング\\システム検証部 証明支援系課\\今井宜洋}
\date{\today}
\maketitle
\tableofcontents{}
%% Coqソースコードを追加削除変更したときはこちらも変更してください
\include{src/Hoge}
\include{src/Piyo}
\end{document}
ターミナルやJenkinsでは次を実行すればよい。
$ coq_makefile -f Make -o Makefile
$ export COQDOCFLAGS="-interpolate -utf8 --body-only"
$ make Proof.pdf
出来上がる生成物(PDF)の例は次のような感じ: https://github.com/yoshihiro503/coqdoc_ja_sample/raw/master/demo/Proof.pdf
また、HTML版の物も次のコマンドで生成できる。
$ unset COQDOCFLAGS
$ make html
出来上がるHTMLは次のような感じ: https://github.com/yoshihiro503/coqdoc_ja_sample/tree/master/demo/html