8
6

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?

More than 5 years have passed since last update.

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

Last updated at Posted at 2015-08-10

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

8
6
0

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
8
6

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?