Agdaに関する日本語論文を書くときのtips
卒論・学会で2度agdaに関する論文を書いたわけですが、TeXとかいう産廃のせいで酷い目に合わされたので、二度とあんなものに時間を取られないようメモを残す。
論文の性質上、ソースコードを載せる必要がある。それに色を付けたいとのことliterate agda(lagda)を使っている。しかしなんとなく使ってまともなpdfが出てくるわけでもない。この記事ではlagdaを使う際の注意点をまとめて書き残す。
まず紹介しておくが、以下のノートはlagdaで作成されており、参考になる。内容はAgdaの入門なので、Agdaについて教えてくれ！な人に投げつけることもできる。
・unicodeに対応せよ
agdaは他の言語に比べて圧倒的に多くの種類のunicode文字を使用するので、日本語かつunicodeを扱えるuplatexを使うこと。同時に、ドキュメントクラスもunicode対応しているか注意し、ujarticleなどを使う。
また、コード中のunicode文字は大抵unicode encoderを使わないとまともに表示されない。やり方は上述したnoteを参考にすべし。
日本語論文だと勝手が違うと思うので、自分がimportしたパッケージを以下に書いておく。どの記事を見てこれを使うに到ったのか今となっては思い出せない。
\usepackage{mathtools}
\usepackage{amsmath}
\usepackage{mathpartir}
\usepackage[utf8]{inputenc}
\usepackage[prefercjkvar]{pxcjkcat}
\usepackage{newunicodechar}
% カテゴリ内のunicode文字を有効化する
% pxcjkcatのドキュメントでカテゴリを確認できる。
% (Vscodeならpxcjkcatをimportしているところの文字にホバーすると見られる)
\cjkcategorymode{forcecjk}
\cjkcategory{sym05}{noncjk}
\cjkcategory{sym08}{noncjk}
% unicode文字の表示方法を教える。
\newunicodechar{⊤}{\ensuremath{\top}}
\newunicodechar{∀}{\ensuremath{\forall}}
・ドキュメントを見よ
小技はドキュメントを探せ
Generating LaTeX — Agda 2.6.3 documentation
・コードの順番を気にせず載せる方法はないのか？
lagdaは、.lagdaファイルからtexに変換する際に、色をつけるコード部分に対し型チェックを行う。間違ったコードを載せてしまう心配はなくなるが、不便なこともある。
例えば、とあるデータ型とそれを使用する関数があった場合、データ型のコンストラクタ定義とそのコンストラクタに対する関数の実装を並べて表示したい、つまり
の順番に説明したいときである。
Agdaのソースコードとしては、このような書き方はParse Errorなので、lagdaはこれをtexに変換させてくれない。これをうまいことやる方法は今見つけていない。仕方ないから、正常なコードを変換させたtexファイルからコード部分を切り貼りして順番をいじるという最悪なことをした。誰かなんとかしてくれ。
・その他
- 矢印は "->" ではなく "→" を使うと文字数が減るので横幅を確保しやすい。
- Agdaのwith句を使うと登場する"|" は コード中のものであってもTeXによって"ー"に勝手に変換されてしまう。クソが。前に論文書いたときは提出前に全部"\mid" に変換するという手間を挟んだ。さきほどAgda documentationの方を見たらなんか解決策っぽいことが書かれていたので試すとよいだろう。
おわりに
lagdaっぽくない色付けをしているAgda論文もあるが、アレは何を使っているのだろう。案外mintとかでうまくいったりするのかもしれない。
ところで、論文執筆にTeXを使わざるを得ない状況はなんとかなりませんかね…
