No Such Blog or Diary

Coq のバージョンを 8.4pl2 から 8.4pl4 に上げたら今まで通っていた証明が通らなくなった．別に用意した lemma を specialize する部分で，lemma の最後の引数を与えるとエラーになるけれど，その手前で止めて specialize した後に最後の引数を与えてあげると通るとかいう意味不明な挙動で……　ちょっと typeclass を入り組んで使っているのでそのせいかもしれないなぁと思いつつ Coq をよく分かっている人に聞いてもやっぱり意味不明とのご回答．とりあえず回避策はわかったので仕事には影響ないけどバグレポートとかするにも挙動再現の最小コードを作るのが面倒そうだというのが最大の問題．

さて，シンポジウムも終わったし後は帰るだけ．

閑話休題．

Albertheijn ってスーパーは夜9時過ぎても開いてて助かった．

パンの上に刺し身……　

機会があればまた食べようと思う程度に美味しかった．

ワークショップ2日目が昼で終わり，次の会議への参加のためにオルレアンからアムステルダムへ移動．パリから3時間しかかからないので電車でＧＯ！

自分の発表が終わったので残りは基本的に観戦モード．次の仕事（作業）の相談とかもしつつだけれども．

そして時差ボケで睡眠時間が平常の 2/3 なので眠い．

閑話休題．

バーガー（やらステーキやら）についてるポテト多すぎ．

JAL Sky Wifi なるものを試す．1フライト（12時間程度）20ドル強．高いんだか安いんだか．

JALカードなら10%割引だけど海外出張2連チャンの航空券を買ったので限度額に引っかかって使えないというオチ．

とりあえず，作ったスライドを git push と叫んでバックアップ取るとかメールの確認するとか VPN 貼ってちょっとデータ取ってくるとかには使える．全体的にもっさりだけど．

明日から海外出張なので財布の中の無駄なものを出してみた．無駄なモノ多すぎ．

とりあえずミスドのポイントカードとか見つかったけれど意味ないよね．

銀だこのも2つも見つかったけど近場ではどこにあるのかわからないね．

オルレアンのトラムの10回券（2年前のもの）も見つかったからこれは持って行こう．