cuspy memo

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 を使うひつようがある。（そのうち対応されるだろうけど。

おしりに火がついてきたのでいいかげん確定申告をする。
e-tax って linux で出来るのか出来ないのか判らないけど、どのみち今から準備するのは間に合わないのでe-tax の準備と、オフラインの書類作成を同時進行でやる。

まず

https://www.keisan.nta.go.jp/h19/ta_top.htm

を開いてみると、このサイトは javascript を有効にしないと進めないので有効にする。

e-tax の準備に進む。
パソコンの推奨環境に linux は含まれていない、解ってたけどね。
でもせめて対応ブラウザに firefox を入れて欲しかった。

次に root CA 証明書のインストールを促された。
ダウンロードしようとすると exe ファイルだった。(2.2Mbyte)
挫折しようとしたところ、「別手順によるルート証明書のインストール」を見つけた。
インストールした証明書は以下の2つ

% openssl x509 -issuer -subject -noout -inform DER -in MOF_Root.cer issuer= /C=JP/O=Japanese Government/OU=Ministry of Finance/OU=MOF Root CA
subject= /C=JP/O=Japanese Government/OU=Ministry of Finance/OU=MOF Root CA

% openssl x509 -issuer -subject -noout -inform DER -in zaimu.cer
issuer= /C=JP/O=Japanese Government/OU=Ministry of Finance/OU=MOF Certification Authority
subject= /C=JP/O=Japanese Government/OU=Ministry of Finance/OU=MOF Certification Authority

次に開始届出を、作成しようとすると、xpdf が起動した。
テキストボックスやリスボックスの様なUI が表示されるけど当然入力出来ないので acroread で開いてみるとこんなエラーが出た。

という訳で、今年は e-tax での確定申告を断念した。
来年また再挑戦してみたい。

確定申告のページのトップから「eTax を使用しない場合又は作成を再開する場合はこちら」のボタンを押すと、URL バーのないウィンドウが新たに開かれた。
これはセキュリティ上問題があるので直して欲しい。

ねむいので続きは朝早く起きて書類を作る。