AgdaでTex、そして日本語 その1
Agdaをさわりはじめてかれこれ2年ぐらいになる。最近ようやく、Agdaの面白さがわかってきて、それを広めたいという気持ちになってきたのでこうしていろいろ書いている。Agdaについてまとまった日本語の情報はあまりに少なく、まとまった日本語の情報がないと現場のエンジニアさんにはなかなか広まらないというのは元エンジニアとしても大変よくわかるので、そのあたりの溝を埋める仕事がしたい。
さて、Agdaを使って論文を書くときにいろいろ問題となるのは、Agdaはunicodeに対応しているのでヘンテコな文字がたくさん使えるのに、論文を書くときに主に使うLaTeXは原則としてはunicodeに対応していないので、いろいろ困るという問題である。最近はunicodeベースのLuaLaTeXとかがあって、その日本語化プロジェクトであるLuaLaTeX-jaなんかもある。そして、それを使うとうまくいくらしい、という話までは聞いているのだけれども、噂レベルでしかなく、うちの教授もちゃんと知らないっぽいので、そのあたりを試行錯誤しているのがぼく。
とりあえずベースとしては、Agda wikiのここ
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.LiterateAgda
から始める。
pTex系で英語でAgdaというのはいろいろすでにうまく使えるみたいなのだが、pTex系で日本語でAgdaというのはかなり苦しいっぽく*1、今回は以下のステップを採用する。
今回は、これからそれを始めます、というだけの前ふりです。
しかし、前述のAgda wikiのページは書いている内容が雑多で、どれがどう関連しているのかわかりづらい・・・まあ、頑張ります。
