No Such Blog or Diary

明日から1時間遅くなるし，せっかくなので早朝のエッフェル塔を見ようと朝5時の電車でパリへ出発．

んで，未明のエッフェル塔のどアップ．東京タワーと違って重たい色なので重量感があっていいと思う．

橋を渡ってシャイヨ宮に移動したところで明け方のエッフェル塔．今日はとても良く晴れてて運が良かった．7時過ぎとはいえまだ暗いしすごく寒いのにちらほら人が来て写真を撮っていたのには驚いた．

そして寒すぎて1時間待機してギブアップ．日の出は拝まずルーブル美術館の地下の開館待ち行列に並んだ．

とりあえず今日も安定して賑わうモナリザ．

金ピカになってる誰もいないアポロンギャラリー．前回は失敗したが今回は混む前に行けた．

そして撮ってる間に人がちらほらきてここらでギブアップ．

最後にニケを ISO200 で撮るオペレーション．混んでるところに露光時間が長いから1時間くらい粘った気がする．その間に幽霊が通ったような写真を大量に生成し，幽霊無しは1枚しか撮れなかった．また今度の機会にチャレンジしよう．

閑話休題．

せっかくなのでユーロコインを錬成しようかと20ユーロ札で切符を買ったら1ユーロコインが18枚出て残念な気分．2ユーロが9枚だと思ってたのに……

幾つかの大学から近めの研究グループが集まって発表しあうローカルなワークショップにお呼ばれして研究の発表をしてきた．ぶっちゃけ「関係のない○○ですが，突然発表します」みたいなノリで．基本的にみんなフランス語で発表するのだけど，私が参加していたせいで何人かが英語で発表してくれたりしてちょっと申し訳ない気分．でも色々とコメントもらえたりして非常にありがたい機会だった．

閑話休題．

参加者のドイツ人にいててお昼時に話をしたので，ついでに俺のドイツ語をチェックしたいんだけどとか言いつつ「Ich komme aus Japan.」と言ったらちゃんとOKをもらえた．バンザイ．とりあえず Ich の ch の発音がよろしいとコメントを貰ったのだけど，国によってはこの音を全然発音できないそうな．少なくとも日本人にはあまり問題ない気がする．

ま，ぶっちゃけ他には数字を数えるくらいしか覚えとらんのだけど．

閑話休題．

Windows 8 が発売されたのか……　何かをポチった記憶があるので実家に何かが届いているに違いない．外装丸出しだとちょっと困るな．

とりあえずセミナー室のプロジェクターはアスペクト比がワイドなのにスクリーンは４：３という……　そしてプロジェクタを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 の決定とのタイミングとかが問題なのか？