No Such Blog or Diary

12月に入って暖房が使えるようになったのだけど，深夜と早朝は暖房が切れるのでやっぱ寒い．なんかこう，部屋にある計算機を全力でぶん回したくなる気分．何か意味のある計算で時間を食うものってあったかな？

つーか家に帰ってコタツで作業するか．みかんがないけれど．

閑話休題．

coqc を動かそうとすると「ライブラリが見つからないから -coqlib で指定しろボケ」と文句を言われる．別のマシンでコンパイルした時にはこんなこと言われなかったので原因がよく分からず今日一日色々と面倒だった．

あー，ちゃんと make install したら問題なくなった気がする．make しただけの状態でパスを通しておいてもダメなのか．バージョン違いを置いとくのにちょっと面倒だな．

NTTにADSL解約の連絡を入れたいのだけどなかなか繋がらない．タイミングが悪いのか？

つーか解約の申込がオンラインでできないとか面倒すぎる．解約するような客の利便性とか考える義理もないだろうけど．

BBIQの工事がやっときたので今日から光回線．8月末に頼んだのでちょうど3ヶ月で開通．まあ，昨日やってた敷地外の電柱のケーブル工事を見た感じだと少なくとも 100m はケーブルを引っ張ってきてたようなので，そこらの許可とか取るのにやっぱ時間かかるのかね．

とりあえず，大学からのファイル転送に 5～10MB/s 出ているので満足．そして google map もストレスなく見られるようになって嬉しい．

さて，要らなくなった ADSL の解約を申込まねば金の無駄だな．これはNTTに直接か．そして今まで使ってた so-net のアカウントは保存しておきたいので接続従量コース（105円/月）にダウングレードするか．

今まで食べたことなかったと思うので注文してみた．かなり香りがあってとても美味しい．

とりあえずそのまま食べても美味しいけれど，あとに残る蜜蝋（巣の基盤部分も蜜蝋だろう）はぶっちゃけ美味しくない．クラッカーと一緒に食べてウヤムヤのうちに飲み下してしまうのがよい？

だがしかし，微妙に高いなぁ．

昨日から寝ずにぶっ続けで24時間超えの時間をかけたら証明が1セット完了した．セミナーでの発表から 3 日遅れか……　間に合わなかったものはまあしょうがない．とりあえず，プログラミングと同様に証明も設計が大事だと理解した．

さて，出来上がった証明に合わせて他の部分を一気に書き換えるか．明日までに完了すれば「11月にやるから！」を守ったことになるだろう．

色々頑張ってるけど結局高いしレンズ微妙なので見送るのが妥当な気がする．このセンサとエンジンを積んだα900作ってくれたら買うのだけど．EVFとOVFをスイッチひとつで切り替えられたりするとなお良い．