自作のシリアル温度計はちょっと心配なので、USB の温度計って売ってないのかなーと探してみた。

* ストロベリー・リナックス ＵＳＢ温度・湿度計モジュール・キット
3,980円
この梅雨の時期、湿度も測定出来るのがポイント高い。
でも残念なことに、windows しかサポートされていない。
HID クラスとして認識するそうなので、がんばれば linux でも扱えそうな感じだけど windows 用の制御ライブラリのソースコードも公開されていないのでちょっと難しいかもしれない。

* メディアラボ USB温度計開発キット
9,800円とちょっと高いけど、linux が用のサンプルコードが公開されているなど linux ユーザーに優しい。湿度センサがついていないのが残念。

* DLP Design DLP-TEMP-G 3-Channel Data/Temperature Acquisition Board
$25.00 輸入になってしまうけど、安い。

とか探してたらこんなの見つけた。
* USBTenki: USB Temperature sensors and more

This project - named USBTenki, from the japanese word ‘tenki’ 天気

なんだこりゃ。
回路図も公開されているし、これぐらいサクッと作れないとダメかなーやっぱり。
この回路図にあるマイクロチップの ATMega8 は 400円程度で売っているので、その他部品を合わせても 1000 円以内で作れそうだな。

原宿の mixi さんで行われた Erlang 分散システム勉強会に行ってきました。
思った以上に参加者が増え、勉強会は定員オーバーで無理でも懇親会だけでも来たい、という方も居たりして大盛況でした。

主催者の井上さん、場所を提供して下さった mixi さん、本当にありがとう御座いました。
普段は滅多に会うことの少ない Erlang スキーな方々や、あの平林さんにお会い出来るな
ど、とても貴重な一日でした。

一応 Dynamo の論文は一通り目を通していたのですが、井上さんの発表を聞いて良く解っ
ていなかった部分が一気に解消する事が出来ました。
バージョニングのアルゴリズムだとか、ノードの同期を取る部分とかで若干マイナーなアルゴリズムが使われてい為、論文を読むだけだと解りにくい部分が多くあってどこから手を付けて良いか困っていたところでした。

TAKESAKO さんの写真館を見つけました。TAKESAKOさんありがとうございます。
http://www.flickr.com/photos/takesako/sets/72157605662821692/

酔っぱらった勢いで erlang-users.jp を取っちゃったけど、これからどうするかはノープランです。

夏が近づき、サーバールーム(押し入れ)の気温がとても気になる。会社に居る時も押し入れの中の気温が気になって仕方がないので押し入れに温度計を仕掛けてみた。

エアコンを付けたり消したりしているので突然気温が低くなっていることが判る。
それでもやたらと高温なのは、温度センサに近いチップが発熱しているからで普通は実際の気温を計測して補正を行わなければならないんだけど本物の気温計を持っていないので補正出来なかった。

これは AVR で適当に作ったシリアルインターフェースの温度計なんだけど、外部電源を必要とするのがダサイので USB で作り直したい。
そしてゆくゆくは、帰宅する 10分前にエアコン入れるとか、湿度が高くなったらドライにするとか、エアコンの自動制御をやりたい。
あと、異常な温度になったら「火事だ!」ってメールを送るようにしたい。

Erlang ベースの WEB サーバー Yaws に Rails を乗っけるというエキサイティングな分散システム Fuzedについて調べようとしてたところ、 gitレポジトリのホスティングサービス github を見つけた。
無料のタイプも有るので後で試してみる。実用でばりばり使うわけじゃないけど、自分で git レポジトリをホスティングする時の参考になるかもしれない。

# というかはやく sourceforge で git を使えるようになれば良いのにな。

せっかく作った 2048bit の秘密鍵も 16bit 相当に縮まってしまうことがある、こんな世の中だから、大事な鍵を生成する時には良質な乱数を使うように心がけたい。 debian の openssl の問題でソースコードを確認してみた所、元々の乱数生成器の実装もどうかと思った。初期化していないメモリの MD5 を反映させているんだけど、初期化してないメモリってかなりの確率で疎なんじゃなかろうか、全部 0 って確率も高いんじゃないかな。
というわけで去年買った eToken Pro にハードウェア乱数生成器がついているので今後大事な鍵はこれを使って作るようにしたい。でもこのハードウェア乱数生成器がその他の疑似乱数生成器と比べて良いという根拠も無いので簡単な検定を行ってみる。
乱数の検定はいろいろ有るみたいだけれど、アメリカ国立標準技術研究所が発行する FIPS 140-2 の中で定義されているものの、何故か打ち消し線で削除されている「monobit test」をやってみる。monobit test とは 20,000 bit の乱数を生成して、1 の数が 9,725 〜 10,275 の間だったら OK、という単純な度数検定。今回は複数の乱数生成器の比較が行いたいのでそれぞれの乱数生成器で生成した乱数からカイ２乗値を求め、比較する。

まずいろいろな乱数生成器で 1M 程度の乱数の生成する。(/dev/random はエントロピーを貯めるのが面倒なのでやめた。)

• /dev/urandom

% dd if=/dev/urandom of=data.urandom bs=1M count=1

• openssl rand

% openssl rand 1048576 -out data.openssl

• eToken Pro HWRNG

% openssl
OpenSSL> engine -t dynamic -pre SO_PATH:/usr/local/openssl/lib/engines/engine_pkcs11.so -pre ID:pkcs11 -pre LIST_ADD:1 -pre LOAD -pre MODULE_PATH:/usr/local/opensc/lib/opensc-pkcs11.so
(dynamic) Dynamic engine loading support
[Success]: SO_PATH:/usr/local/openssl/lib/engines/engine_pkcs11.so
[Success]: ID:pkcs11
[Success]: LIST_ADD:1
[Success]: LOAD
[Success]: MODULE_PATH:/usr/local/opensc/lib/opensc-pkcs11.so
Loaded: (pkcs11) pkcs11 engine
[ available ]
OpenSSL> rand -engine pkcs11 1048576 -out data.etoken

って生成した乱数のχ２乗値を求めてみたんだけどやっぱりダメだこれ、何回やっても値がバラバラで。サンプル数を増やしても値が収束しない。
一気にやる気が失せてしまったけれど、また今度別の検定方法で挑戦するかもしれない。

これは、クロスケーブルを作りたいけど圧着ペンチを持ってないという方やストレートケーブルはそこら辺にごろごろ転がっているのにわざわざクロスケーブルを買うのは勿体ない。という方に向けたチュートリアルです。

1. ストレートケーブルの外皮を剥きます。



2. 緑とオレンジ、あと緑白のスプライトとオレンジ白のスプライトの線を切ります



3. 緑とオレンジを結線し、緑白のスプライトとオレンジ白のスプライトを結線します。



4. 完成。

この様に、ネジネジしただけだとショートする可能性があるので不安な人は半田付けして、ガムテープでも巻いておくと安心です。

昨日の続きで runit をさわってみる。
run script と同じ所に finish という名前の script を置くことで異常終了時にメールを送ったり出来るって書いたけど、sv down でサービスを計画終了させた時にも finish script は実行されるみたい。
正常終了と異常終了を区別するにはどうしたら良いか調べてみると finish script に 2つの引数が渡って実行されていることが解った。

finish script の内容を

#!/bin/sh

echo $@

こんな感じにして、sv down すると

-1 15

という内容がログに書き出された。
たぶん、1つ目はプロセスの終了コード(main の返値)で 2つめはシグナルの様だ。
なので異常終了時にメールを送りたい時は

#!/bin/sh

if [ $2 -ne 15 ];then
# メールを送る
fi

というような finish script にした。

runit は daemontools と同様のプロセスのスーパーバイザシステム。
daemontools が public domain になって久しいけど、今後の機能拡張やインターフェイスの改善が期待出来ないので手近なところから runit に乗り換えてみた。
インストールドキュメントを読んでて強烈な既視感を感じたけど、無事動作することが出来た。

ちょっと使ってみて気がついた良いところ

* finish script
プロセスが異常終了した時にメールを送ったり

* svlogd(multilogの代替) で syslog に飛ばせる
multilog では logger に渡して変なことやってたなぁ

* log に tai64n じゃなくて人間に読みやすい普通の日付を入れられる
でも、ローカルのタイムゾーンに出来ないのが不満。

かっこいいシステムモニタの conky を普通に実行すると、描画の度にチラついて鬱陶しい。設定ファイル .conkyrc に

double_buffer yes

と書いたとしても

Conky: drawing to single buffer

という標準エラー出力が出ていることからダブルバッファリングが有効になっていない事が解る。これを有効にするには X.Org の double-buffering extension を使う必要があることが解った。
/etc/X11/xorg.conf の Section “Module” に

Load “dbe”

って書いた。これで conky がチラつなかなくなった。
でも逆に今まで使っていた torsmo が見えなくなったんだけど、それはもういいや。

zsh の colors が便利、これを使うと .zshrc が大分シンプルになった。
通常赤色を表示する場合

% echo -e “\e[31mhello"

という記号めいた文字を記述しなければならないが、zsh の colors を使うと

% autoload -U colors
% colors

というように有効化して

% echo -e "${fg[red]}hello”

で赤色の文字が表示される。バックグラウンドを赤色にするには

% echo -e “${bg[red]}hello”

foreground と background を一般化すると

% echo -e “\e[${color[red]}mhello”
% echo -e “\e[${color[bg-red]}mhello”

でも良い。
使用出来るキーは

% echo $color
none normal bg-blue 31 bold no-standout bg-magenta faint no-underline bg-cyan standout no-blink bg-white underline 33 41 01 blink no-reverse bg-default 27 no-conceal reverse conceal 30 31 08 39 02 32 24 45 35 05 34 30 39 47 black 23 red green 43 yellow 36 blue magenta 37 cyan 03 white 44 35 default 40 28 07 46 04 33 37 40 22 34 42 00 30 30 25 49 bg-black 36 32 bg-red bg-green bg-yellow

で確認出来た。

いい加減、太古のバージョン管理システムCVS から脱却したいので git への完全移行を目指す。Software Design の４月号に git の記事があったのでざっと読んでみた。git のフロントエンドは cogito を使うのが一般的かと思ってたんだけど、最近はそうでもないらしいので素の git の使い方を覚えることにした。

% apt-get install git-core

として git を実行すると、

[hamano@kujira]% git
git, the filemanager with GNU Interactive Tools, is now called gitfm.

If you are looking for git, Linus Torvald’s content tracker, install
the cogito and git-core packages and see README.Debian and git(7).

This transition script will be removed in the debian stable
release after etch.

If you wish to complete the transition early, install git-core
and use (as root):
update-alternatives –config git

Press RETURN to run gitfm

こんな感じで怒られるけど、これは GNU Interactive Tools が同じ git コマンドだかららしい。

% update-alternatives –config git

There are 2 alternatives which provide `git’.

Selection Alternative
———————————————–
*+ 1 /usr/bin/git.transition
2 /usr/bin/git-scm

Press enter to keep the default[*], or type selection number:

ここで2ばんを選ぶと本当に使いたい git が使えるようになった。

手始めに .zshrc や .emacs などのホームディレクトリ以下の設定ファイルを git で管理してみる。通常のソースコードの管理と違うのは

% git clone /git/dotfiles.git ~
destination directory ‘/home/hamano’ already exists.

というように設定ファイル群をホームディレクトリ以下にぶちまけようと思っても既にディレクトリが存在していると失敗してしまう。なので

% git clone –bare /git/dotfiles.git ~/.git
% git checkout

というように –bare オプションを付けて裸の .git レポジトリをホームディレクトリに置いて checkout するとよさそうだけど、残念なことに origin ブランチが無い事に気がついた。origin ブランチを手動で追加する方法が解らなかったので(.git/remotes/を直接触れば出来そう、1.5以降では git remote というサブコマンドが在るようだ)

% git clone /git/dotfiles.git tmp
% mv tmp/.git ~
% git checkout

というようにしてホームディレクトリ以下に設定ファイルを展開した。これで git pull で origin ブランチとの同期が取れるようになった。
これからじわじわと git に移行していく予定。

WordPress 2.5 RC2 が出ていたので人柱になってみた。
正式版がでたら他の人の分もアップデートする予定。
見た目はなーんにも変わってないけど、管理ツールががらりと変わっていていろいろ便利になっているのでみんなも使いたいと思うはず。

上の方にあるのはサカさんが書いてくれたロゴ、カッコいいけどどっかで見たような気がするなぁ。元々の絵はキレイだったんだけど gimp で縮小したらギザギザになって台無し。

あと permlink を変えようと思ったんだけど既存の permlink に影響が出ないように変更するのがムリっぽくて断念した。
permlink は変わらないからこそ permlink なんだけど、コメントとトラックバックが打てないそもそもの原因は、permlink が関係しているので何とかしたいなー。

自動証明処理系の coq を使って簡単な3段論法を証明してみる。

まず coq を起動する。

% coqtop
Coq <

命題 A B C について考えてみるよ。

Coq < Variables A B C : Prop.
A is assumed
B is assumed
C is assumed

「A ならば B 」というのは命題だよね?

Coq < Check (A -> B).
A -> B
: Prop

じゃあ簡単なトートロジー「A ならば B ならば C」ならば「A ならば B」であり「A ならば C」を証明するよ。

Coq < Goal (A -> B -> C) -> (A -> B) -> A -> C.
1 subgoal

============================
(A -> B -> C) -> (A -> B) -> A -> C

導入する。

Coq < intro H.
1 subgoal

H : A -> B -> C
============================
(A -> B) -> A -> C

いっぺんに同時に導入できるよ。

Coq < intros H’ HA.
1 subgoal

H : A -> B -> C
H’ : A -> B
HA : A
============================
C

仮説 H を適用します。

Coq < apply H.
2 subgoals

H : A -> B -> C
H’ : A -> B
HA : A
============================
A

subgoal 2 is:
B

仮説 HA は正しいよ。

Coq < exact HA.
1 subgoal

H : A -> B -> C
H’ : A -> B
HA : A
============================
B

そして H’ を適用します。

Coq < apply H’.
1 subgoal

H : A -> B -> C
H’ : A -> B
HA : A
============================
A

Coq < assumption.
Proof completed.

証明終わり。

うー、もっとカッコイイ証明をいろいろやってみたいんだけど圧倒的に脳みそが足りない。

土曜の夜。sige君が「純米大吟醸寒しずく」をどこからか大量に仕入れてきた。
限定 3000 本しか売ってないはずなのにこの部屋に 10 本もあるなんて!
(写真にあるように瓶にはロット番号が打ってある)
起きたら、2本しか残って無くてガッカリした。(3人しかいなかったよね？
# 酔っぱらった人たちは中国国内から great firewall を超える為の技術的方法とビジネスモデルについて朝まで話してた様な気がするけどあまり思い出せない、議事録を取らないとダメだな。
昼に起きてそのまま PHP 拡張勉強会に行く
頭が痛くて呂律が回らなかったような気がするけどうまく喋れただろうか。
ustream で撮って頂いた様なので後で探す。

http://events.php.gr.jp/event.php/event_show/39

その後飲み会。お疲れさまでした!

なんとなく GNU tar のソースコードを読んでたら、LZMA オプション発見。
最近 GNU のプロダクトで .tar.lzma ってファイルを見かけるようになったのでいつか tar で扱えるようになるだろうなと思ってたところ。
tar-1.19 ではまだ対応して無くて tar-1.19.1 のスナップショットから使えるみたい。

ftp://download.gnu.org.ua/pub/alpha/tar/tar-1.19.1-20071030.tar.gz

今のところ -a オプションだけど今後変更されるかもしれない。

static struct zip_magic const magic[] = {
  { ct_none, },
  { ct_compress, 2, "\037\235", "compress", "-Z" },
  { ct_gzip,     2, "\037\213", "gzip", "-z"  },
  { ct_bzip2,    3, "BZh",      "bzip2", "-j" },
  { ct_lzma,     6, "\xFFLZMA", "lzma", "-a" }, /* FIXME: ???? */
};

中では lzma を clone(2) するので予め lzma をインストールしておく必要がある。
# debian だと apt-get install lzma

これで、

$ tar cvaf dir.tar.lzma dir

と言うように lzma の tar アーカイブを作成することが出来るが、まだ展開は対応してない様なので unlzma を使うひつようがある。（そのうち対応されるだろうけど。