coqdocで日本語を含むPDFを生成する

3782 ワード
coqdoc ProofCafe Coq platex Coq テキストリンク

Coqのドキュメント生成ツールであるcoqdocはコマンドラインオプションによってHTML形式やPDF形式の書類を生成するが、PDF形式の書類を作成する際に内部でpdfTeXを使っているようで、日本語を含むソースコードを扱う場合は簡単にはうまくいかないことがある。

そこで、coqdocからはtex形式のファイルを出すところまでやってもらい、残りはplatexなど自分の好きな方法で処理したい。

次のような内容のMakeというファイルを追加すればわりと簡単に実現できる(CoqのソースコードはHoge.v, Piyo.vだとする)。

Make
-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は自分で用意する。例えば次のような感じ。

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