はてなブログ

移行するのか使い分けるのか決めずに始めましたが，移行する気がしています． http://eagletmt.hateblo.jp/

p.twimg.com 以下の文字列

Twitter for iPhone や Photobucket を利用して画像を上げると，画像は p.twimg.com/*.jpg というような場所に置かれる． このパスの部分の文字列がどうやって生成されているのか気になった． しばらく観察してわかったことは 15文字固定 使われる文字は英数…

推論規則をレイアウトする bcprules.sty

LaTeX

今まで推論規則を書くときは proof.sty を使っていた． \[ \infer[\mbox{\sc T-App}]{ \Gamma \vdash t_1\ t_2 : \tau_2 }{ \Gamma \vdash t_1 : \tau_1 \rightarrow \tau_2 & \Gamma \vdash t_2 : \tau_1 } \] と書くと のようにレイアウトされる． しかし…

補完リストの高さを調節したり表示・非表示をトグルしたり

Vimperator

例えば 'autocomplete' を有効にして :ec commandl と入力すると，:ec co の段階で多くの補完候補が表示され，そのときの高さを保ったまま :ec commandl の補完候補が表示された状態になる． これは特にページのコンテンツを見ながらコマンドラインを入力し…

記号の幅をいいかんじに揃える

LaTeX

LaTeX で BNF 的なものを書くときに，::= や | の記号をいいかんじに揃えたい．縦に並べるだけなら eqnarray 環境でやればいいかんじに揃う． \begin{eqnarray*} t &::=& x \\ &|& t + t \\ &|& t - t \\ &|& t \times t \\ &|& t \div t \\ \end{eqnarray*}…

ハッシュの衝突

http://events.ccc.de/congress/2011/Fahrplan/events/4680.en.html おもしろい． ウェブアプリケーションフレームワークのほとんどはパラメータを勝手に解析してハッシュテーブルに突っ込んでいるけど，ハッシュが衝突するようなキーを意図的に大量に送りつ…

unite-haddock 書いた

Haskell Vim

http://d.hatena.ne.jp/kitokitoki/20111217/p1 の「ghc-browse-document の anything 化」が便利っぽかったので同じようなものを書いた． https://github.com/eagletmt/unite-haddock ghc-mod が必要．cabal install ghc-mod でインストールできる．Vim 内…

grundy number

Algorithm

grundy number について知ったのでメモ．これは ある完全情報ゲームについて，両プレイヤーが勝つために最善の状態遷移を選択したとき，与えられた初期状態から先手が勝つか後手が勝つかを答えよ． というような問題を解くときに使えるかもしれない考え方．…

ランタイムに失敗しないインデックス演算子

Haskell

前回の発展のようなかんじで，GADT を用いて型レベル自然数同士の大小関係を表現する項を作れるようにし，「n が m より小さい」ことを示す項と Vec m a を受け取って n 番目の要素を返す関数を定義してみた． 例によって一度ランタイムに compare して LT, …

ランタイムのチェックを一度で済ます

Haskell

http://d.hatena.ne.jp/Lost_dog/20111128/1322504143 reify_integer がおもしろいなーと思った． これと同じ雰囲気で， dependent type の例によく出てくる「長さ n のベクトル型 Vec n a」についてこんなのが書けそう． 同じ長さ n のベクトル同士だけ zip…

GHC API を使ってある型コンストラクタのデータコンストラクタを得る

Haskell GHC

neco-ghc などで，Haskell 用の補完候補をより正確に計算するときに活用できないかなーと思った． GHC 7.0.3 で試した． あるモジュールがエクスポートしている名前は modInfoExports でとれる． そのモジュールで定義されていれば modInfoTyThings で TyThi…

型エラーとして FizzBuzz を出力

Haskell

GHC で以下のコードをコンパイルしようとすると，型エラーとして FizzBuzz 的なものが出力されます． 出力を見やすくしようとして Template Haskell を使ったら比較的最近の GHC でないとコンパイルできなくなってしまった… 手元の GHC (7.0.3) だと OK で，…

ext3 から ext4 へ

Arch Linux

パーティションの内容を保持しつつ ext3 から ext4 へのマイグレーション． 今回はルートパーティションの /dev/sda7 について作業した． 基本的には ArchWiki に書いてある通りに． https://wiki.archlinux.org/index.php/Ext4#Converting_ext3_partitions_…

プログラミングコンテストの記録

そういえばこんなかんじにネタバレを書いてます． http://eagletmt.github.com/contests/ POJ, AOJ を中心に，AC したコード + 簡単な解法の説明． 今のところ POJ 200問くらいと，AOJ 30問くらいを書いてる． まぁ自分の実力は高くないので，どれくらいの人…

uim-skk で server completion

SKK

そういえば，以前書いたパッチ http://d.hatena.ne.jp/eagletmt/20110615/1308162572 がちゃんとまともに書き直されて，本家のリポジトリに取り込まれました． http://code.google.com/p/uim/source/detail?r=7278

夏ゼミ2011

大学

9月8日から10日まで，諏訪湖の近くで行われた研究室の夏ゼミに参加していた． 各自が情報工学に関する何かについて自由に発表するというもので，俺は型レベルプログラミングについて話した． FunctionalDependencies, FlexibleContexts, FlexibleInstances, …

C80

院試が控えているので(?)ビッグサイトへは行かなかったけれども横浜のメロンととらへは行った． 比較的読みたい度が高くて店頭で見つけられたものから．なんと5冊． 現地行くとおまけ貰えたりグッズとかもちょっと買ったりするんだけど，そういうのが一切な…

Linux 3.0 で SBCL 1.0.50 が起動直後に Segmentation fault する問題

Arch では Linux 3.0 が core に入った． http://www.archlinux.org/news/changes-to-kernel-package-and-filenames/ これに関連してドライバの問題やブート時の問題が結構 bug tracker に報告されているけど，自分の環境ではそういった問題は起こっていない…

Arch Linux で PT2 (DVB 版ドライバ earth-pt1 + fuse_b25)

Linux PT2

以前 Arch Linux での PT2 環境のセットアップをまとめた．そこでは chardev 版のドライバを利用していた． http://d.hatena.ne.jp/eagletmt/20110307/1299492620 が，BKL が削除されたことによって最近の Linux だとそのままではコンパイルできなくなってい…

ICPC2011 国内予選

haskell-lover というチームで参加していた．メンバーは俺と id:osa_k と id:draftcode． 結果は全体で10位，学内で1位になれました． http://icpc2011.ait.kyushu-u.ac.jp/icpc2011/common/guest_standings_ja.php http://imoz.jp/icpc/2011-domestic.html …

uim-skk で server completion を利用する

SKK

http://gihyo.jp/admin/serial/01/ubuntu-recipe/0175 で SKK の server completion というものを知った． yaskkserv + DDSKK でそれなりに便利なかんじだったので，uim-skk でも使えるようにするパッチを書いた． https://github.com/eagletmt/uim-skk-serv…

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

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

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 [] と書け，という話はまぁよく例として聞く気…

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

Vim Coq

http://www.iij-ii.co.jp/lab/techdoc/coqt/ を読んでいたらいつのまにかそんなかんじのを書いていた．どうしても Vim で書きたいかわいそうな人以外は普通に CoqIDE や Proof General 使ったほうがいいと思います． https://github.com/eagletmt/coqtop-vim…

ssh 活用

dynamic port forwarding ssh -D 1080 remotehost とか，~/.ssh/config に Host remotehost DynamicForward 1080 と書いて ssh remotehost すると，1080番ポートで SOCKS プロキシサーバを立てられる． firefox のような SOCKS プロキシに対応したソフトウェ…

きょうのめんま

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 $DAT…

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

PT2

してみた． http://d.hatena.ne.jp/eagletmt/20110307/1299492620 で recpt1 が死んでいたのは，/dev/pt1video* を close(2) した直後に open(2) すると，終了処理に時間がかかっているのかそのデバイスが使用中のときと同じように EIO で失敗するのが原因だ…

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

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

gem2arch

Arch Linux Ruby

実家に帰ってきているんだが，対応を誤って輪番停電により下宿のマシンが起きてこなくなってしまったためやることが無くなり，なんとなく gem を Arch のパッケージマネージャで管理しようとした． 同じような PKGBUILD を手動で書くのはタルいので cabal2ar…

Arch Linux で PT2

Linux PT2

PT2 を手に入れてしまったので Arch Linux で使えるようにした作業メモ． マシン環境は % uname -a Linux reinforce 2.6.37-ARCH #1 SMP PREEMPT Fri Feb 25 07:53:43 CET 2011 x86_64 Intel(R) Core(TM) i3 CPU 530 @ 2.93GHz GenuineIntel GNU/Linuxカード…