2011-06-02

Ricty のビルド中に fontforge が segmentation fault でクラッシュする問題

ホームページで触れられているのは Mac OS X についてだけが，Linux においても Ricty のビルド中に fontforge がクラッシュする環境がある．
http://save.sys.t.u-tokyo.ac.jp/~yusa/fonts/ricty.html
どうやら RemoveOverlap() という操作の最中にクラッシュしてるっぽかった．

いろいろ調べてみると，--enable-double をつけずにビルドした fontforge ならクラッシュしなかった．
Debian の fontforge パッケージは，Ricty ではないけどフォントのビルドに失敗するという理由で過去に --enable-double が外されていたようだ．
http://bugs.debian.org/cgi-bin/bugreport.cgi?bug=609094
Arch Linux の fontforge パッケージは，--enable-double を外してもらったので 20110222-2 以降ならクラッシュしないはず．
Mac OS X では試してないが，homebrew の formula を見てみると --enable-double しているので，これを外してビルドすれば同様にクラッシュしなくなるかもしれない．

追記 2011-06-02T16:24:52

Macports で入れた fontforge だとクラッシュしないという話を聞いたので見てみると --enable-double はなかった。
http://trac.macports.org/browser/trunk/dports/graphics/fontforge/Portfile
やはり Mac OS X においてもこのオプションを外すことでクラッシュしなくなると思われる。

2011-05-17

reverse

Coq

関数型言語で reverse を書くときは

let rec reverse1 = function
  | [] -> []
  | x::xs -> reverse1 xs @ [x]

ではなく

let reverse2 =
  let rec aux xs = function
      | [] -> xs
      | y::ys -> aux (y::xs) ys
  in aux []

と書け，という話はまぁよく例として聞く気がしますが，はじめての Coq なかんじでこの2つの reverse が等価，つまり reverse1 xs = reverse2 xs であることを証明してみた(たぶん)．

Require Import List.

Fixpoint reverse1 {A : Type} (xs : list A) :=
  match xs with
    | nil => nil
    | x::xs => reverse1 xs ++ x::nil
  end.

Fixpoint reverse2_aux {A : Type} (xs ys : list A) :=
  match ys with
    | nil => xs
    | y::ys => reverse2_aux (y :: xs) ys
  end.
Definition reverse2 {A : Type} (xs : list A) := reverse2_aux nil xs.

Lemma app_assoc : forall (A : Type) (xs ys zs : list A), (xs ++ ys) ++ zs = xs ++ (ys ++ zs).
Proof.
  induction xs.
  reflexivity.

  intros.
  simpl.
  f_equal.
  apply IHxs.
Qed.

Lemma rev2_app : forall (A : Type) (ys xs : list A), reverse2_aux xs ys = reverse2_aux nil ys ++ xs.
Proof.
  induction ys.
  reflexivity.

  intros.
  simpl.
  rewrite IHys with (xs := a :: nil).
  rewrite app_assoc.
  simpl.
  apply IHys.
Qed.

Theorem reverse_eqv : forall (A : Type) (xs : list A), reverse1 xs = reverse2 xs.
Proof.
  unfold reverse2.
  induction xs.
  reflexivity.

  simpl.
  rewrite IHxs.
  symmetry.
  apply rev2_app.
Qed.

2011-05-15

coqtop を Vim の中で動かして連携させる

Vim Coq

http://www.iij-ii.co.jp/lab/techdoc/coqt/ を読んでいたらいつのまにかそんなかんじのを書いていた．どうしても Vim で書きたいかわいそうな人以外は普通に CoqIDE や Proof General 使ったほうがいいと思います．
https://github.com/eagletmt/coqtop-vim
最新の vimproc を先にインストールしておく必要がある．

使い方としてはまず :CoqStart で coqtop からの出力を表示するバッファとウィンドウを作る．

コードを書いていき，インサートモードでするとその行まで coqtop に送られる．ノーマルモードで :CoqGoto あるいは g *1でも同じ．

既に送られた領域の最後の行は Folded で色付けされ，これより上の行は編集できなくなる．
(ところで「編集できなく」するために今は CursorMoved,CursorMovedI でカーソル行をチェックして 'modifiable' を変更する，という方法でやっているけど，ある領域だけ完全に編集不可能にする方法はあるんだろうか．現状の実装だと undo とか setline() とかで簡単に編集されてしまう．編集されると :CoqGoto による巻き戻しが破綻する．)

一度送ってしまったけれども間違えたと思ってやり直したいときは，

戻りたい行にカーソルを合わせて :CoqGoto あるいは g で，その行まで巻き戻される．

coqtop が受け付けるコマンドの一部も Vim のコマンドとして提供している．
今はとりあえず

:CoqPrint (Print に相当)
:CoqSearchAbout (SearchAbout に相当)

が使える．

まだ安定性に不安が残るので，もしなにか挙動がおかしくなってきたら :CoqClear または c でクリアしてください．

*1: はデフォルトでは \ だと思う．詳細は :help maplocalleader で

2011-05-04

ssh 活用

dynamic port forwarding

ssh -D 1080 remotehost とか，~/.ssh/config に

Host remotehost
DynamicForward 1080

と書いて ssh remotehost すると，1080番ポートで SOCKS プロキシサーバを立てられる．
firefox のような SOCKS プロキシに対応したソフトウェアなら，localhost:1080 を SOCKS プロキシとして設定すれば，remotehost からアクセスしているように振舞える．

活用方法としては例えば研究室内からしかアクセスできないページがあるとき，ssh -D 1080 研究室してプロキシを通せばアクセスできるようになる．
あるいは普通は用意されたプロキシを通じないと外へアクセスできないけど ssh なら素通りできるような場合，ssh -D 1080 自宅してこれを通してアクセスするようにすると幸せになれたりする．

SOCKS プロキシに対応したソフトウェアは少なく，wget なんかでも使えない．
そういうときは tsocks が使える．LD_PRELOAD で一部関数を上書きしていいかんじにやってくれる．
tsocks - Transparent SOCKS Proxying Library
tsocks の他に socksify というのもあるらしい．

DynamicForward の他に LocalForward や RemoteForward といった port forwarding がある．

ProxyCommand

hostA には外側からアクセスできるけど hostB には内側からしかアクセスできない状態で，外側から hostB にアクセスしたい場合．
ssh hostA の後に ssh hostB すれば可能だけど

わざわざ2回 ssh する必要がある
hostA と hostB の間にも鍵が必要

といった面倒さがある．

こういうときは ~/.ssh/config に

Host hostB
HostName hostB
ProxyCommand ssh hostA nc %h %p

と設定しておくと，ssh hostB で hostA を踏み台にして hostB に繋げるようになる．
ssh の他に nc が必要になるが，おそらくほとんどの環境で使えると思う*1．
HostName に設定した hostB は hostA からでないと解決できないような名前でも問題ない．
鍵による認証は localhost <-> hostA 間と localhost <-> hostB 間で行われる．

セッションを共有

~/.ssh/config に

ControlMaster auto
ControlPath ~/.ssh/master-%r@%h:%p

とか設定しておくと，UNIX socket が作られて同一サーバへのセッションが共有されるようになる．
複数 ssh するときにログインが不要になるので早くなる．
また scp とかするときに zsh は引数を補完するたびにリモートにアクセスしてしまうので，一定時間内の ssh 要求をセキュリティ等の目的で制限しているとその制限にひっかかり悲しい思いをする，というようなことを防ぐ効果もあったりする．

切断

ssh 上で ~. と入力すると接続を切ることができる．
ネットワークの不調で ssh が止まったり，うっかり大量に端末に出力するコマンドを実行してしまったとき等に有効．
この ~ は escape character であり，設定で変えたり無効化したりもできる．

sftp

リモートとのファイルのやりとりは scp や rsync なんかも使えるが，インタラクティブにやるときは sftp が便利．
ftp と同じように cd とか ls とか get とか put とかできる．

他に sshfs で mount するという手もある．それなりに高速な回線環境ならシームレスにリモートのファイルを扱える．

現在の俺の ~/.ssh/config はだいたいこんなかんじになってる．
設定がうまく反映されないなーというときは ssh -v の出力を眺めたりする．
~/.ssh/config に書いた設定は ssh コマンドだけでなく，scp や sftp，git を ssh 経由で利用するとき等にも適用される．
その他様々な設定は man 5 ssh_config に．

# 自宅
Host srv1 srv1-proxy
HostName srv1.example.net
User eagletmt

# VirtualBox 内にある FreeBSD に ssh freebsd でも入れるようにしたりとか
Host freebsd
HostName 192.168.56.101
User eagletmt

# 外から見えるサーバ
Host srv3 srv3-proxy
HostName srv3.example.com
User eagletmt

# srv3 経由でしか入れないサーバ．srv2 という名前は srv3 で解決される．
Host srv2
HostName srv2
User eagletmt
ProxyCommand ssh srv3 nc %h %p

# ssh なんちゃら-proxy としたときには DynamicForward 1080 するように
Host *-proxy
DynamicForward 1080

# 一般的な設定
Host *
ServerAliveInterval 60
ControlMaster auto
ControlPath ~/.ssh/master-%r@%h:%p

*1:Arch では gnu-netcat パッケージに入ってる

2011-04-24

きょうのめんま

http://www.anohana.jp/menma/index.html

#!/bin/sh
DATE=$(date +%m%d)
rtmpdump \
  --rtmp "rtmpe://fms30-cache.stream.ne.jp:1935/aniplex-bc/_definst_/sound/anohana/menma_$DATE" \
  --swfUrl 'http://www.anohana.jp/menma/voicePlayer.swf' \
  -o $DATE.flv

# ffmpeg -loglevel quiet -i $DATE.flv -vn -acodec copy $DATE.mp3

2011-03-28

recpt1ctl --channel に対する recpt1 の動作を改良

PT2

してみた．
http://d.hatena.ne.jp/eagletmt/20110307/1299492620 で recpt1 が死んでいたのは，/dev/pt1video* を close(2) した直後に open(2) すると，終了処理に時間がかかっているのかそのデバイスが使用中のときと同じように EIO で失敗するのが原因だった．それに加えてデバイスファイルから read(2) できなかった場合に，確保したバッファの解放を忘れているためにメモリを食い潰して殺される，というかんじだったようだ．
いろいろ試してみると close(2) せずに SET_CHANNEL してもチャンネルを変えられるっぽかったので，デバイスファイルを使い回せる，つまり地デジ同士か衛星放送同士のチャンネルの切り替えなら SET_CHANNEL するようにした．ただし残念なことに自分は衛星放送を視聴できる環境にないので，これで本当に問題が無いのか検証できていない．
https://gist.github.com/890635

2011-03-23

ja_JP ロケールにおける wctype(3)/iswctype(3), wctrans(3)/towctrans(3)

wctype(3) は引数として渡された名前に対応した property を返し，これを利用して iswctype(3) である文字がその property を持っているかどうか判定する．どんな property があるかはロケールに依存しているが，alnum, alpha, blank 等の全てのロケールで使えるものもある．これらの property による判定はそれぞれよく知られている isalnum(3), isalpha(3), isblank(3) 等と同じ．

wctrans(3)/towctrans(3) は似たようなインターフェイスで文字の変換を行う．全てのロケールで使えるものは tolower, toupper で，それぞれ tolower(3), toupper(3) にあたる．

で，日本の ja_JP ロケールにおいては /usr/share/i18n/locales/ja_JP を見てみると wctype(3) に渡せる名前として

jspace
jhira
jkata
jkanji
jdigit

が使え，wctrans(3) には

tojhira
tojkata

が使えるみたい．

とりあえず手元の Linux 環境と ideone で以下のコードが意図した通りに動いたけど，どれくらい広く利用可能なのか，*BSD 系でも同様に動作するのかは知らない．
http://ideone.com/7kWcM

#include <stdio.h>
#include <stdlib.h>
#include <locale.h>
#include <wchar.h>
#include <wctype.h>

static void sample_wctype(const wchar_t *str, const char *name)
{
  const wctype_t wc = wctype(name);
  if (wc == (wctype_t)0) {
    fprintf(stderr, "wctype(%s) is not supported in this locale\n", name);
    return;
  }

  const size_t len = wcslen(str);
  size_t i;
  for (i = 0; i < len; i++) {
    wprintf(L"is%s? %lc => %d\n", name, str[i], iswctype(str[i], wc));
  }
}

static void sample_wctrans(const wchar_t *str, const char *name)
{
  const wctrans_t wct = wctrans(name);
  if (wct == (wctrans_t)0) {
    fprintf(stderr, "wctrans(%s) is not supported in this locale\n", name);
    return;
  }

  const size_t len = wcslen(str);
  size_t i;
  for (i = 0; i < len; i++) {
    wprintf(L"%s %lc => %lc\n", name, str[i], towctrans(str[i], wct));
  }
}

int main(void)
{
  if (setlocale(LC_ALL, "ja_JP.UTF-8") == NULL) {
    fputs("setlocale failed\n", stderr);
    return 1;
  }

  const wchar_t str[] = L"廾ゃヵ";

  sample_wctype(str, "jkata");
  sample_wctype(str, "jkanji");
  sample_wctrans(str, "tojkata");

  return 0;
}