2015/03/01

Agda のソースコードを listings で LaTeX に埋め込む

LaTeX で Agda のソースコードを含む pdf を作ることに。
他のソースコードは listings で埋め込んでいたけれど、Agdaで使っている特定の文字が化けて表示されない。
verbatim でも表示されないので、Agda のソースを LaTeX 用にエスケープして、記号処理は LaTeX に任せることで listings できるようになったお話。

環境

  • Mac OS X 10.9.5
  • MacTeX 20140525

埋め込み方法

listings の escapechar を設定して、表示されない記号を LaTeX 用に置換してあげる。
escapechar が @ で、≡ を置換したかったら @$\equiv$@ みたいな。
escapechar の中は LaTeX 環境になるので、$ で数式を直接書いてしまえばok。
スクリプトとかは以下。
.agda から置換した .eagda を生成してくれます。
LaTeX からの参照は .eagda を指定してます。




周り道とか

Literate Agda ってのもあるみたいです。
lagda で書いておけば LaTeX としても認識してくれるっぽい?
でも今回は使わない方向でいきました。
本来Agdaのソースを埋め込むのならこっちなのかな。

あと大きなソース(500行くらい)のやつを LaTeX に食わせるとメモリが足りなくて落ちる時が。
! TeX capacity exceeded, sorry [main memory size=5000000].
とか言われる。
/usr/local/texlive/2014/texmf.cnf に
main_memory=8000000
extra_mem_bot=8000000
font_mem_size=8000000
pool_size=8000000
buf_size=8000000 
とか書いたら動いた。
メモリの制限とか自前で持ってるのね TeX。

あと、utf8周りでもメモリ周りでも LuaTeX 良いよって指摘があった。
LuaTeX 使うのも良いのかもしれない。
ちなみに今回は platex 使いました。

あとは listings 側のオプションに escapeinside とか literate とか使えそうなのもあったけれど動かず。
これはどうしてなのだろう。
ウムラウト付きの文字なら literate できます、みたいなのは記事にあったんだけれど ≡ は置換されず。

参考文献

ギー沖解散パーティーに行ってきました

2014/02/21 にギークハウス沖縄解散パーティーがあったので参加してきました。

ギー沖の3周年+解散パーティーでした。

人がかなり来ていて、多い時には30名以上いたみたいです。
ギー沖に関わっている人って多かったのだなー、とつくづく。
お隣りさんも来たりして、ネットは広いのだか狭いのだか。

メインディッシュは豚の丸焼き。
始めて食べたのですけれど部位によって硬さとか油とか変わるので若干探検っぽい。
しばらく販売が止まってたカーリーフライを久々に見たりもしました。

ギー沖LTがあって、これまでのギー沖の思い出とか突然の brain fu*k の話とか。
brain fu*k の話があるならー、ということで飛び入りでAgdaの話をしてきました。

LT ではあまりギー沖の話をしなかったのでブログに書こうかと。
ギー沖、何かの動機で1週間くらい泊まったことが(2012/02 くらいだっけ?)。
そんなこんなでギー沖に行くようになって、 Okinawa.rb の weekly meetup にも参加。
私が Ruby を勧める時の「はじめてのプログラミング」 -> 「たのしいRuby」 -> 「メタプログラミングRuby」の流れは Okinawa.rb から来てたり。
初心者組がメソッド分からんって言ってる時に横で libkinjo さんがメタプロの話とかしていたよーな。
Okinawa.rb で hanachin さんと関数型の話して、結果的に Agda 書いてたりするので、Ruby に触れるのも Haskell やら触っているのも元はギー沖から来てるかも。
思えば libkinjo さんのみゅーたんとか tompng さんの Ruby で lisp interpreter できるよねー、とかぱかなさんのギー飯とかこたにんさん飯とか、思い返すといろいろとありますね。

イベントもたくさんあったし、人もたくさんいた場所でした。
ありがとうギー沖。