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 できます、みたいなのは記事にあったんだけれど ≡ は置換されず。

参考文献

LaTeX/Source Code Listings - Wikibooks, open books for an open world

unicode - Having problems with listings and UTF-8. Can it be fixed? - TeX - LaTeX Stack Exchange

encoding - Listings in Latex with UTF-8 (or at least german umlauts) - Stack Overflow

QED symbol in latex - Stack Overflow

TeX capacity exceeded, sorry · matlab2tikz/matlab2tikz Wiki · GitHub

Makefileの書き方に関する備忘録 - minus9d's diary

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

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 できるよねー、とかぱかなさんのギー飯とかこたにんさん飯とか、思い返すといろいろとありますね。

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

私の git の参考文献とか使い方とかまとめ 2014

git どうやって勉強したのさー、って質問が。
参考になるかはともかく私の最近の git の使い方についてまとめてみます。
このコマンドはどういう挙動をします、って話ではなくて、どんな時に使う、くらいのまとめです。
調べるためのキーワード提供にでもなれば。

参考文献とか考えとか

• staging とか workspace とか commit とか : どこだっけ。ちょっと覚えてない。
• rebase とか –no-ff の知識 : こわくない git かな。 基本的に git の話するときはこれを勧めてます。
• tips とか : ここ とか。必要になったら調べる感じ。
• branching model : 過去のログを見るとここを参考にしてたみたい
• branching model : 複数人数で git を使う時の自分の中ルールだと
  • master には直接 commit しない
  • origin/master への push -f は最終手段
  • merge は master に対して –no-ff
  • conflict の解消は branch での rebase で解決する
  • github を使ってるなら merge は pull request で、 conflict したら branch で rebase 
• commit message とかの話 : ChangeLog を支える英語

基本的に使うコマンド

• git init
  • リポジトリ作る。
• git ( add | mv | rm )
  • ファイルの追加とか移動とか削除とか。
• git st
  • status を見る。面倒なので alias かけてます。
• git commit
  • コミット。
• git log
  • ログを見る。2.0 くらいから特に設定しなくても色が付くようになってうれしい。
• git diff (–cached)
  • diff を見る。
  • diff で commit と workspace 間の diff。 add してなかったらこっち。
  • diff –cached で commit と staging 間の diff。 add した後に diff りたかったらこっち。
• git fetch
  • remote から変更を取ってくる。
  • commit してない変更がある時とか、ローカルブランチで作業してる時に変更が欲しかったら fetch
• git pull
  • remote から変更を取ってくる + 変更を反映する
  • master で変更を取ってきたいなら pull で良いかな、くらいの使い方
• git clone
  • リポジトリを clone する
  • github は https:// を clone すると毎回 password 聞いてくるので git:// で clone すると楽
• git merge (–no-ff)
  • branch を merge する
  • 私は master には直接 commit せずに –no-ff する主義。
• git branch (-a | -d | -D )
  • ブランチを見たり作ったり
  • -a で remote も含め全部。
  • -d で削除。 -D で強制削除。
• git co ( -b | -f )
  • checkout する。面倒なので alias かけてる
  • 最近 branch するのが面倒なので -b を良く使う気がする
  • 作業前の状態にしたいやー、って時は -f を使う。
  • stash でも良いけれど本当にいらないと思うときはこっち。
• git reset
  • add したやつを戻す。
  • soft reset, hard reset がある
• git rebase -i
  • rebase は -i を良く使うかも
  • master から派生した branch にいる時は rebase -i master が楽
  • conflict したら –abort 諦めるくらいの軽さで commit の入れ替えとかたまにやる。
  • 最近は commit –amend するより commit して rebase -i で fixup とかする
  • fixup と rewind で –amend みたいなことができるし良いかなーといった感じ
• git remote ( add | rm )
  • そんなに使わない
  • clone すると origin があるので基本はそれを使ってる
  • fork したリポジトリの upstream を設定する時くらい

あると便利

• git grep
  • リポジトリ内を grep する
• git ls-files
  • リポジトリに入ってるファイルの一覧
• git remote prune origin
  • remote に無い branch を local でも消してくれる
  • branch -a がうるさく無くなるのでちょっと快適
• git reset –hard
  • 最終兵器。
  • 間違って master に commit した時に checkout -b して reset –hard HEAD^ とか便利
• git reflog
  • rebase, merge にミスった時はコレ
  • reflog 漁って git reset –hard で大体解決する
  • ので gc は設定で切ってたりします。コマンド打つと勝手に gc して止まるのも何だし。
• git stash ( pop | apply |save )
  • workspace の変更を一時保存
  • 軽量 commit みたいなものだけれど最近は commit + rebase してしまうかも
  • この実装でいけるか怪しいけれど一応は保存しておきたい、くらいの時に save するかなー、くらい
• git bisect
  • エンバグした時に便利
  • 動いてた時と動いて無い時を指定して、動かなくなった commit を特定するやつ
  • これをまともに使うためにも master は必ず動く状態の commit のみで構成したい理由はコレ
  • コンパイル通らない、とかだと bisect できない
• git cherry-pick
  • 特定の commit を拾ってくるやつ
  • master に特定の commit があるなら rebase で拾うけれど
  • 欲しい commit が他 branch でそれ以外の commit を拾いたく無い時とかに使う
• git archive
  • repository を zip とかにできる
  • なんか提出する時とかに使ってた記憶。そんなに使わないけれど特定の人達には需要あるかも

ghc 読み会に参加してみた

コンパイラの講義で行なわれた ghc 読み会に紛れ込んできました。2014/12/06と07。

まずは ghc の内部構造の話から。
ここ を参考にしながら ghc がどのような流れでバイナリを吐くのか、みたいな話とか。
まずは Core に変換されて、STG に変換したあと LLVM なり gcc なりのバックエンドで実行コードを吐く、みたいな流れみたいです。
Core は Haskell でついてる型からどうやって Primitive 型に変換するか、みたいなのも処理する様子。
あと型変数とかも処理するので、関数に型を渡したりもできる言語っぽいです。
ほとんど Agda みたいに見える。
case で実行するので、 case を使う場所によって遅延評価にしたり正則評価にしたり変えられるみたい。
Core の定義そのものはシンプルっ。Exprは6種類しか無いとか。
ただ ghc 自体は 200k 行とかあって、シンプルな言語だとしても処理系側でカバーしてるだけなのかなー、とか。Core しかり Haskell しかり。
あとは Haskell はグラフだぜー、とか要素いろいろ。良い資料っぽさげ。

次に実際にデバッガで追っていこう、ということに。
Vagrant で box 作ってその中で実行したのでログとか。

• $ vagrant init chef/ubuntu-14.04
• $ vim Vagrantfile
• メモリとか CPU 割り当てとか編集
• $ vagrant up
• $ vagrant ssh
• $ sudo apt-get update
• $ sudo apt-get install git cabal-install vim
• $ sudo apt-get build-dep -y ghc
• $ vim ~/.bashrc
• export PATH=$HOME/.cabal/bin:$PATH
• $ source .bashrc
• $ cabal update
• $ cabal install cabal-install
• $ cabal install happy alex
• $ git clone git://github.com/ghc/ghc.git
• $ cd ghc
• $ ./sync-all -r git://github.com/ghc get
• $ perl boot
• $ ./configure --with-ghc=/usr/bin/ghc
• $ vi mk/buil.mk
• buildFlavor を devel2 に
• GhcDebugged = YES を末尾に
• $ make MAKE="make -j" -j
• 1時間くらい。付けなかったら3時間とかかった
• $ sudo make install
• $ ghci -fobject-code -cpp -DSTAGE=2 -I. -I./stage2 -I./stage2/build -illvmGen:prelude:cbits:specialise:stranal:coreSyn:stgSyn:basicTypes:main:stage2:iface:simplCore:simplStg:cmm:types:codeGen:typecheck:profiling:parser:rename:utils:nativeGen:hsSyn:deSugar:ghci:vectorise:stage2/build: main/DriverPipeline.hs
• すると .o ができる
• DriverPipeline は読みたいので DriverPipeline.hi を消して
• $ ghci -cpp -DSTAGE=2 -I. -I./stage2 -I./stage2/build -illvmGen:prelude:cbits:specialise:stranal:coreSyn:stgSyn:basicTypes:main:stage2:iface:simplCore:simplStg:cmm:types:codeGen:typecheck:profiling:parser:rename:utils:nativeGen:hsSyn:deSugar:ghci:vectorise:stage2/build: main/DriverPipeline.hs
• で b compileFile できる
• $ s <- SysTools.initSysTools (Just "/usr/local/lib/ghc-7.9.20141205")
• $ env <- HscMain.newHscEnv $ DynFlags.defaultDynFlags s
• $ DriverPipeline.compileFile env (DriverPhases.Hsc DriverPhases.HsSrcFile) ("/home/vagrant/hoge.hs", Nothing)

とりあえず compileFile って関数があるので呼んでみよう、というログが上のもの。

ghc の main を直接 ghci で実行すると、「今呼んだらもう遅い」みたいな abort で落ちたので main 以外を実行しようとして見つけたのが compileFile 。

stage 2 の ghc の library とかを使って ghc の DriverPipeline.hs なるソースを読もうとしたログ。

読もうとした時に問題発生。

そもそも Haskell ってどうデバッグしたり追っていくものなのだろう、という疑問。

調べると ghci が出るんだけれど、 ghci の trace って読むために使うものだろうか。

とりあえずそれ以外の選択肢は無かったので ghci で実行してた。

実行することはできたのだけれど問題がいくつかあって

• -I の指定順とか結構謎。オプションの順番変えると動かないとかあったり。
• .o がある .hs を ghci で読み込むと、そのファイルの関数に break point が付けられない
• けど -boot file は .o が無いと参照できないので .o を作らないといけないソースもある
• 実行するためには HscEnv とかが必要なのだけれどそれを作るのが大変

とか。追おうにも追いづらい。

test から見ようにもテスト単位がユニットごとじゃなくて全体用のテストのみで単体の動作を追うのも無理。

Haskeller の人達ってどうやってデバッグ やソースコードリーディングしているのだろう。

あと、小さい単位に分けたりしなくても大丈夫なのだろうか。テストとか。HscEnv とか。(値が20個とかある型だった)

型チェックとかでどうにかしてるのかなー。その辺りの情報が謎。

ghc の Travis とか見たら結構 build コケてたりしていて実際どうやってるのか不安。

最後には Parser や Lexer をソースから読むことに。

Alex とか Happy とか使いつつ。

Parser も実際に動かすことはできなくて、 Haskeller はどうやってデバッグしてるんだろうか、というところでタイムアップ。

結局 Haskeller はどんな風にデバッグしたりソース読んだりテストしたりするのだろう、という疑問が募っておしまい、という感じ。

Core の構造とかを知ることができたのが収穫かなー、といったところ。

コーディングを支える技術 を読んだ

コーディングを支える技術 ~成り立ちから学ぶプログラミング作法 を読みました。

プログラミングにおける機構の成り立ちとかを解説してくれる本でした。
if 文は何故あるの、関数は何故あるの、型は、スコープは、... みたいなことを「こういう経緯があって、この言語はこういうアプローチで解決した」という歴史を教えてくれる。なので、機構の名前と機能だけを解説するのではなく、むしろこういう経緯があったんだよー、って話の方がメイン。

取り上げられているトピックも多岐に渡ります。表紙に書かれている要素を列挙すると、演算子、繰り返し、関数、例外、スコープ、動的型付け、型推論、配列、辞書、スレッド、ロック、トランザクショナルメモリ、クラス、インターフェース、継承、委譲、C3線形化、Mix-in、トレイト となっています。かなりの範囲をカバーしてそう。

あと、複数の解決方法を知ることができるので、言語Aの機構Bは言語Cの機構Dと似ててここが違う、とかが分かるのも良いところ。例えば Ruby の Hash は、他の言語では Dictionary  だったり HashMap だったりとか。

さらにおもしろかったのは、同じ単語に対して異なる解釈があること。
私は Ruby をよく使っているので「オブジェクト指向」と言えば「オブジェクトにメッセージを送ることによってオブジェクトそのものに振る舞わせる」ことだと解釈するのですが、C++では「オブジェクト指向」と言えば「ユーザ定義型であるクラスによる処理の再利用」となっていたり。オブジェクト指向に限った話で言えば Perl での処理の共通化、 JavaScript での prototype など、言語による解釈や実装がいくつもあるのだなー、と。

読む前は「オブジェクト指向はクラスだ」という言葉は「なんでメッセージの話が出ないんだろう」と思いましたが、「(ある言語における)オブジェクト指向はクラスだ」みたいに主語が隠れてるんだろうなー、と。
そういう意味でも、自分の知ってる言語の機構名だけで考えるんじゃなくて成り立ちを知ることや他の言語を知ることには利点がありそうだなー、とか。

この本で機構そのものを学ぶというよりは、今までそんなに意識せずに使っていた機構にまつわる経緯は何なのか、とかを知る本です。
なので、ある程度プログラミング言語に触ってから読むと、おまじないにしていた謎が解けたりするかもしれません。
プログラミング言語の勉強の始めに読むのには向いてないけれど、言語の勉強に詰まった時や歴史を知りたい時とかに読むのが良さそう。