No Such Blog or Diary

大学で明日の発表の準備．Expression Templates 使ったライブラリの技術的な話を期待さられているらしいのだけど，実装されたものを紹介しても複雑すぎるので簡易版を作って説明しなければならない．

ということで，朝からガリガリとC++のテンプレートなコードを書きつつスライド作成．ひと通り作ってから整理したら何故か２話分のスライドが出来上がっていた．

閑話休題．

休日の防犯巡回か何かの人たちがやってきて何かを語りかけられたのだけど，ぶっちゃけ何言ってるかわからんかった．ジェスチャー的に鍵をちゃんとかけろってことだと思うのだけど，正確なところはわからない．つか，フランス語分かりませんって言うフランス語を喋れるようになるべきだな．英語で言っても通じない．

「日本語食べれません」って言えば大抵の人は引き下がるよ，とかいうことを言っていた留学生を思い出した（「喋れません」すら言えないと認識されて無罪放免になるという論理）．

さくらのVPS以外も試してみようと思って，L2TP/IPsec な VPN が簡単に作れるかどうか幾つかの安い VPS で試した．つか，VPS と VPN って紛らわしい．

とりあえず月490円のお安い DTI の ServersMan @VPS Enrty を最初に試したが，使えるUbuntu のバージョンが古い（10.10 amd64, 10.04 x86）ってのと，カーネル周りがどうやって弄ったものかわからないのとで使いにくい．カーネルモジュール全然ないし……　モジュールを作りなおすとか嫌すぎるし……　そもそもカーネルいじれるのか？　Ubuntu でカーネル変えると起動しませんとか書いてあるドキュメントもあったり……　とかいう感じで即解約．そもそも Ubuntu のインストーラを自分で操作してインストールするタイプでないので色々と面倒．

次に，月840円のカゴヤの VPS タイプA を試すも基本的に ServerMan のと同じでカーネル周りの自由度が……　という感想で即解約．こちらはインスタンスを１日30円で簡単に増やせるのでその点は便利な気がする．

最後に月940円のお名前.com のVPS1GBプラン．これは普通に Ubunru 12.04 を Ubuntu のインストーラを使ってインストールできるのでさくらのVPSと同様に使いやすい（さらには自前のISOをマウントして起動できるのか？）．んで，通常のインストーラで入れるのでカーネル周りも普通で L2TP/IPsec な VPN の構築も何の問題もなく終わった．さくらの VPS と比べてコントロールパネルの出来がよろしい（初心者向けな）気がする．

とうことで，結論：お名前.com の VPS は使いやすいっぽい．計算機性能はどうだかしらんけど．

閑話休題．

お名前.com でサービスを使うには電話認証が必要だったりして微妙に躓いた．申請完了通知のメールに書いてあるURLのページに行ってそこにあるボタンを押すと，申請時に書いた電話番号に電話がかかってくるので，そのページにある認証コードを電話で入れてくださいと．……出張中にもかかわらず自宅の電話番号で申し込みをすると電話認証ができず残念なコトに．とりあえず，ユーザ情報の変更で携帯の電話番号に変更した上でもう一つインスタンスを申し込んで認証をするとかいう対処をした．つか，普通に電話番号間違って登録することもあるだろうから何処かに真っ当な対処法が有る気もする．

Haskell と違って型以外の項もパラメータにとれるので色々と遊べる．自動でプログラムを変換させてみたりとか（基本となる関数の変換方法をインスタンスとして置いといて，それらの基本関数を適当に合成したものの変換結果を計算させるとか）．

とりあえず基本的なギミックは理解したので来週はもうちょい応用にチャレンジしよう．

閑話休題．

自明だけど証明が面倒（というか tactic の使い方に慣れてない）なので admit が大活躍してたりする今日この頃．慣れている人が証明してくれることを願いつつリポジトリに投げる．

Coq に「Hoge a b c の項が期待されるのに Hoge a b c の型の項なのでエラー」と言われた．このメッセージだけを見ていても何も悪いことしてないようにしか思えない．

んで，Set Printing All. と叫んでみたら implicit なパラメータ部分で微妙にずれていたという罠で，「@Hoge X a b c の項が期待されるのに @Hoge Y a b c の型の項なのでエラー」という意味のわかるエラーを吐いてくれるようになった．

……見えている型が同じだったら隠れている部分も自動で表示してくれればいいのに．

いい場所にキッチン付きのホテル（アパートメントホテル）を見つけたので移動．目の前に大学直通のトラムの駅がある．まぁ，３０分強かかるけど．

とりあえずキッチンが使えるのはいいことだ．

1998年～1999年 Slackware．最初に Linux をいじった時にはカーネルのバージョンはまだ 2.0.X だった．PJE で Wnn を突っ込んだりとかしていたような気がする．この頃に比べると最近はものすごく便利になったもんだ．

1999年～2000年 Turbo Linux．ここらで Slackware で環境整えるのが面倒になって Turbo Linux に手を出してひよった．研究室のマシンは FreeBSD だったっけな．まだまだ Linux は趣味の世界だった頃？

2000年～2005年 Red Hat＆Fedora Core．ひよるのにお金かけるのもあれだからとフリーにもどる．しばらくは Red Hat 系で安定．

2005年～2006年 Gentoo．後輩が使っているのを見て使い始めた気がする．結局，色々と面倒になったのとコンパイルしまくるのは環境によろしくないのとで１年くらいしか使わなかった気がする．

2006年～2008年 Debian．ここらは使うディストリビューションを色々試しつつ Fedora より Debian のほうが使いやすいかなぁとか考えていた気がする．

2008年～2012年 Ubuntu．お仕事用のメインマシンを Linux にして生活しようと決めて，色々と楽な Ubuntu に移ったのが 2008年の頭だったはず．ここから基本的に Ubuntu しか使ってない．

うん，よくわからんが普通な変遷だ．