2014年1月24日金曜日

arch linuxでcrosstool-ngを使ってppc64bitのクロスコンパイラを作る

yaourtが入っていることを前提とする.

yaourt -S crosstool-ng
mkdir -p ~/cross/bin
cd ~/cross/bin
ct-ng list-samples
ct-ng <選んだsample>
ct-ng menuconfig

ここで設定するわけだが要点は以下の様になる

  • いらないものは削る
    • gcjとか普通のひとはいらない.
  • ライブラリはできるだけ新しいものを選択する.
    • バージョンが古いとarchのgccではあたらしすぎてコンパイルできなかったりする
  • C-Libraryの Force unwind supportはcheckする
    • しなかったらコンパイルエラーがでた
  • gdbでpython scriptingをenableにしない
    • archのpythonは3系だが,python2系を前提としているらしく,どうせgdbでpythonを使わないので面倒だから無効にしてしまった

次に

ct-ng build

でコンパイルを始めるが,make4.0だとあたらしすぎてglibcのコンパイルが通らない.そこで http://lfsbookja.sourceforge.jp/svn.ja/chapter06/glibc.html にもあるように

sed -r -i 's/(3..89..)/\1 | 4.*/' configure

でglibcのconfigureを変更する必要がある.一回ダウンロードが済んだあとで止めて修正すればいいはず.

これで

ct-ng build

でコンパイルが通って~/xtools以下にそれらしきものが入った.

2014年1月15日水曜日

bashでtestを使うと遅いよ

bashでは


if [ $a -eq 0 ] ...

と書く代わりに


if [[ $a -eq 0 ]] ...

と書ける。test([,])は外部コマンドだから評価のときに毎回forkして遅いような気がする。一方[[,]]は内部コマンドだからforkしなくて速いのではないかと思ったのでベンチマークを取ってみた。

ベンチマーク


for a in $(seq 1 100000) ; do [ 0 -eq 100 ] ; done
for a in $(seq 1 100000) ; do [[ 0 -eq 100 ]] ; done

結果

real    0m0.535s
user    0m0.517s
sys     0m0.017s

real    0m0.353s
user    0m0.347s
sys     0m0.007s

予想通り[[,]]の方がまあまあ速かった。因みに[[,]]の方では正規表現マッチなど機能が追加されている。互換性を追求するなどの理由がない限り[[,]]を使った方が良さそう。

2014年1月2日木曜日

ひとり正月Coq勉強会

以前も若干勝手にCoqを勉強したことはありましたが,その時は直感主義論理の簡単な証明を書いたくらいで時間がなくなってしまいました.今回は非常に簡単ながら証明駆動っぽい開発をやってみました.なお,Coqはほぼ書いたことがないので証明とかアレかもしれない.

  • やってみたかったこと : 非常に簡単な証明駆動開発
  • 題材 : cons
    • sortとかマジな証明だとちゃんと小1時間で終わらなくなってしまうので,本当に簡単なものをやってみた

consしたら

  • head $ cons x xs = x になる
  • tail $ cons x xs = xs になる

の2つの性質が満たされる.ということで命題を書いてみた

Definition is_head_x (A : Type)( x :option A) ( xs : list A) : Prop := (head xs) = x.
Definition is_tail_ys (A : Type)( ys :list A) ( xs : list A) : Prop := (tail xs) = ys.

そして consを定義

Definition cons ( A : Type) ( x : A) ( xs : list A) : list A := cons x xs.

証明はdefinitionより明らかなのでunfoldするだけで,わざわざ書く価値もないが,とりあえず.適当に証明して.

Extraction Language Haskell.
Extraction cons.

でHaskellのconsを適用するだけの関数が出てきた.

非常に簡単すぎてこれでいいのかよくわからないが,多分証明駆動開発の最も短い実例になったと思う.