No Such Blog or Diary

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 の切り替えもできてないような？

という言葉が一瞬通じなかった．Daylight saving time でオッケーだったと．

Wikipedia の Daylight saving time を見たらアメリカ英語的には daylight saving time なのね．"summer time" って言い方はイギリス英語であると．まあ，Daylight saving time より summer time の方が単純な単語を使っているから日本だとサマータイムってなるのかね．

閑話休題．

つまり月末の土曜の深夜で終わりなんだな．前回来た時とは逆向きの調整になるのか……　一日が２５時間になるはずだけどどの時間帯が重複するんだろう？