No Such Blog or Diary

とりあえずセミナー室のプロジェクターはアスペクト比がワイドなのにスクリーンは４：３という……　そしてプロジェクタを4:3出力した時にちょうどスクリーンいっぱいに映るようにしているのでワイド画面なPCを普通に接続すると両端がはみ出す罠．どうにかして欲しい気分．

なんとなくワイドに対応した横長のスクリーンってまだあまり見たことがない気がする．

閑話休題．

改めて部屋を眺めてみると日本の製品があちこちにあるのね．問題のプロジェクタもパナソニックだし．前に座ってる人が使ってたPCは東芝だし．ホテルのエアコンはダイキンでテレビは東芝だし．こんなもんなのか．

Isabelle チュートリアルがあったので参加．Coqと違うなぁと思いつつ具体的にどう違うのかわからない程度．ハマったのは from a and b show hoge とか書いて a と b の順番が逆だと証明できないとかいうオチで．and って書いたら普通 commtative だと思いたいのだけどそうではないと．

つーか動きがよくわからん．当たり前だが．

閑話休題．

ディナーが７時半に始まり１１時に終わるとか時間かけすぎだと思うのは気のせいだろうか？　そして炭水化物が足りない．

閑話休題．

SNFC でストか……　どれくらい続くのかよくわからんのでちょっと遠出しにくいなぁ．満月直後にモンサンミッシェルとか行こうかと思ったが来週もう一度とかやられると困る……

モジュールがぁとか叫びながら Coq と遊んでいたらいつの間にか朝になっていたのでそのまま大学へ．同じファンクタを同じモジュールに別のモジュール内で適用してやったものが別物として扱われているのか何かの問題で物事がうまくいかない（訳わからんことしとるなぁ）．つか，モジュールのシステムをリファレンスとか見ずに直感で使っているからおかしなことになっているのかもしれない．依存関係がめちゃくちゃなのをどうにかしよう．

閑話休題．

さすがに typeclasses のサーチの時間がかかりすぎるようになってきたなぁ．プログラムの自動変換が終わるまで30秒待ってくださいってのはギャグでしかない気がしてきた．

Proof General で Compile Before Require のオプションを使っているのだけど，たまには rm *.vo *.glob してやったほうが良いのかもしれない．とりあえず意味不明な挙動が解消された気がする．……気がするだけかもしれない．

つか，Proof. typeclasses eauto. Qed. で証明できるのに証明が必要とかわけわからん．いまひとつ typeclass のリゾルバの挙動がつかめん．Implicit arguments の決定とのタイミングとかが問題なのか？

兎にも角にもめんどくさすぎてやってられん．つーか typeclass でライブラリ全部書き直されないかなぁ．

閑話休題．

モジュールの読み込みとインスタンス宣言のタイミングとの兼ね合いで個々の機能は動くのに合成した機能が働かない．いまひとつモジュールを絡めたスコープの扱いがよくわかってないな．要修行．

そして今日も無限ループと戦う．

Typeclass の eauto の深さ指定ができない．Typeclasses eauto := debug bfs 10 とかかくと 10 のところはピリオドだろと怒られる．うーん，書き方が悪いのか廃れたオプションがマニュアルにあるのか実装してないのにマニュアルにあるのか……

とりあえず，よくわからんけど無限ループしまくるのをどうにかして欲しい．デバッグも大変．すんごく微妙にインスタンスの優先度を設定したら無限ループを回避できたけど，もうちょっと頭良く探索してくれないかなぁ．

つか，dfs と bfs の切り替えもできてないような？