Agda を HEAD から build する

brew で gcc と ghc の version を上げたら Agda が build できなくなったので repository から build したおはなし

環境

• Mac OSX 10.9.4
• Homebrew 0.9.5 (bd3217ea598e9ccf85bb5b1f5ac244f1641378f8)
• gcc 4.9.1
• ghc 7.6.3 (brew 的には 7.6.3_3)
• cabal-install 1.20.0.2 (installed by homebrew)
• cabal-install 1.20.0.3 (installed by cabal-install)

経緯

一旦 cabal を消して gcc と ghc の version を上げる

• brew uninstall haskell-platform
• brew upgrade gcc
• brew upgrade ghc
• rm -rf ~/.cabal ~/.ghc
• brew install haskell-platform

そして cabal で agda を入れる

• rehash
• cabal update
• cabal install cabal-install
• rehash
• cabal install agda

と、こんなエラーが。

src/full/Agda/Utils/Cluster.hs:50:10:
    Duplicate instance declarations:
      instance Monad m => Functor (EquivT s x y m)
        -- Defined at src/full/Agda/Utils/Cluster.hs:50:10
      instance Functor m => Functor (EquivT s c v m)
        -- Defined in ‘Data.Equivalence.Monad’
cabal: Error: some packages failed to install:
Agda-2.4.0.1 failed during the building phase. The exception was:
ExitFailure 1

調べてみると依存パッケージの equivalence に 0.2.4 から Agda と重複する内容が入ったらしいです。

解決方法としては equivalence を downgrade するか Agda の該当部分を排除しろ、とのこと。

HEAD からの build と haskell-platform からの脱却

stack over flow に書かれてるっぽいのでおそらく HEAD では修正されてないかなー、ということで repository を落としてみる。

• cabal info agda

の Source Repo に github があったのでそれを clone。

あと brew 側で haskell-platform ではなく cabal-install を使ってみたり。

何故か依存が自動インストールされなくて happy と alex を入れたりもした。

結果的に実行したコマンドは以下な流れ。

• cabal install happy
• cabal install alex
• git clone https://github.com/agda/agda.git
• cd agda
• ./configure
• make

make すると cabal install が走ってくれるみたいで結果的に実行ファイルがきちんと .cabal に入ってた。

ちなみに記事を書いた時点での HEAD は a11a5fb9fc8421747f50d0280c3afe650acd4f1b で Agda の versioning は 2.4.1 扱いになってました。

brew で gcc の install から実行するとなると

• brew install gcc
• brew install ghc
• brew install cabal-install
• rehash
• cabal update
• cabal install cabal-install
• rehash
• cabal install happy
• cabal install alex
• git clone https://github.com/agda/agda.git
• cd agda
• ./configure
• make

ってな感じでしょうか。

とりあえず Agda 2.4.1 がリリースされれば問題無く build できるはずなので、それまでの間で発生しちゃう問題っぽさそうです。

3Dプリンタを使ってHDD用のスタンドを作ってみた

縦置きのHDDを買ってみたは良いものの、スタンドがある訳でも無くて若干不安定っぽい。
専用スタンドがある訳でも無いのでどうせなら作ってみよう、ということで3Dプリンタで作ってみました。

3Dプリンタでは .stl というフォーマットのファイルをプリントできるっぽいです。
.stl は3つの座標を指定して作成できる三角系の組み合わせでモデルを構成しているらしいです。
その .stl を ruby で生成する コード を @tompng さんが作ってくれていたので、本人に許可を取って拝借して HDDスタンドを生成するスクリプトを作ってみました。ありがとうございます。

3Dプリンタは某工学部にあるものをお願いして使わせてもらいました。ありがとうございます。

こんな感じ

「無いなら作れば良いじゃない」感あって便利。

オープンキャンパス2014

2014/07/19 に オープンキャンパスがありました。

今回は

• Programming3 で作品3つ
• OpenCV で光を認識してレーザーポインタで絵が書ける
• 丸を認識してダンボーを表示するAR
• Kinect でお絵描き
• IGDA琉球大学からゲームとかの紹介
• 研究室より分散ネットワークフレームワーク Alice

を展示してました。

参加者は午前が多め。午後は少なめでした。

午前は人が多かったので、ポスターなりなんなりがあると良さげかなー、とかやってました。

• デモが見られない人用にディスプレイの横にポスター置くとか
• あとディスプレイはミラーリングして横に置いてるだけでも見える人増えそう

実際見てる側がどうだったのかはちょっと分からないけれど。

あとは午後は人少なめだったので、テンプレみたいなのができあがってた

あっち行ってー、次はあっちでー、みたいな

私としてはブースの配置とか説明して好きなところ行けー、みたいなことをしたかったれどコントロール大変そう。どっちが良いんだろうなー。

今回は「はーい実行委員通りまーす。はーい実行委員でーす」ってな感じで連絡とかそういったことがメインで発表とかは無しでした。

みなさん協力的だったのでありがたかったです。

さて来年は誰が来ますかねー。あと programming 3 の作品もどうなることかな。期待ですね。

ポインタの話をしていたらいつの間にか 配列の初期化 とか glibc の printf とかを読んでいた話

2014/07/13 にとつぜん @y0t4 さんと「ポインタを一年生にどう解説するか」みたいな話をしてたと思ったら想定外に長話 + 長旅になったのでつらつらと。

char* の初期化の話

C で char* を初期化する時に

とかするじゃん、という話になって、これはどう動いているかというと

• (char *) の hoge が作られる
• "" なのリテラルがメモリに展開される
• その先頭アドレスが hoge に代入される

という話になって、それじゃ実証しよう、ということで 

• a.out を objdump -d
• main とか探すと
•   4004cc:       48 c7 45 f8 e8 05 40    movq   $0x4005e8,-0x8(%rbp)
• とかしてるので、 0x4005e8 くらいが怪しいだろう、と
• objdump -D して  0x4005e8  を見ると
• 4005e8:       66                      data16
• 4005e9:       75 67                   jne    400652 <__dso_handle+0x72>
• 4005eb:       61                      (bad)  
• となっているので "fuga" っぽい。
• [2] pry(main)> 'fuga'.chars.map{|c| c.ord.to_s(16)}
• => ["66", "75", "67", "61"]
• ちなみにこのアドレスは .rodata っぽいっすね。
• ということで、 "" は一旦どこぞに展開されてからその先頭アドレスが返る、という認識であってるやー、という一段落

char[] の初期化の話

とまでなったところで、じゃあいわゆる「ポインタなんて配列とほとんど同じだよー」なんて発言に対抗することに。

char[] の初期化だと

とかするじゃん、ということで char* の初期化との違いは?ってなことに。

実行すると fuga が出ることは同じなんだけれど。

• a.out を objdump -d してみると
• 4004c8:       48 83 ec 10             sub    $0x10,%rsp
• 4004cc:       c6 45 f0 66             movb   $0x66,-0x10(%rbp)
• 4004d0:       c6 45 f1 75             movb   $0x75,-0xf(%rbp)
• 4004d4:       c6 45 f2 67             movb   $0x67,-0xe(%rbp)
• 4004d8:       c6 45 f3 61             movb   $0x61,-0xd(%rbp)
• 4004dc:       c6 45 f4 00             movb   $0x0,-0xc(%rbp)
• こっちは "fuga" を register に入れてってる
• ということで配列の初期化は要素が1個1個入れられていってる
• "" みたいに data として確保されるわけじゃなくて、各要素ごとに処理をしている

ということに。

なので char* はあくまで変数は char* のみで、そこに rodata にある "" のアドレスが入ってる。

char[] は array として確保されてる領域に 1つ1つ入れてる。

ちなみに私は C に string って無いから "" の syntax 自体無いものだと思い込んでいて、内部的に char[] に変換されるような拡張が gcc とかにあるようだと思ってたけれどオプションでは見つけられなかった。

どうなってるかは C99 の仕様とかを読んだ方が良いのかも。

printf の呼び方

ということで、 "" は実際は先頭アドレスとして扱える、というところまで来て、 printf に渡す "" はどうなってるの、ということに。

結局 "" で渡しているので、の中身本体は rodata にあるのだけれど、printf 関数に渡してるのは pointer だから、pointer 渡せるのでは、ということでやってみる。

動く上に当然ながら第一引数の中に %p とかが入っていても展開される。

となった時に、第二引数消したらどうなるの、ということに。
-Wall すると「printf に引数足りないよ」って言われるけれど、ポインタで渡してるからそんなのチェックしてないだろうし、ということでこんなコード。

そして実行。すると毎回違う値が出てくる。

指定してる先が無いはずなのに nil とかじゃなくて違う値が出てくるのはどうして、ということになった。

そして glibc へ

じゃあ printf 読もうぜ、ということになって glibc を読むことに。

yota さんが「最近 glibc make した」とのことで手元にソースが。

printf は stdio.c の中にあると思ったらそうでもなく、  stdio-common にありました。

• ptintf.c がある
• vfptinrf に stdout を渡してる
• たぶん va_start が可変長引数なんだろうなー
• vfprintf.c に vfprintf がある
• このあたりから大量のマクロが
• vim の syntax highlighter の色が変
• 何気に tabstop=8 の世界
• あとマクロなので設定上1行
• これメンテ大変なのでは
• そして読んでると jump_table ってものが
• 見るとこれが %s とかの分岐先らしい
• つまり jump_table にあるのが printf の format option だということっぽい
• ちなみに JUMP_TABLE_TYPE に飛び先があるっぽいですね
• これによると REF form_pointer へ jump するっぽい
• LABEL (form_pointer): から奥
• fspec の値によって va_arg から取ってくるか args_value から取ってきて ptr に入れる
• va_arg の方は読んでない
• たぶん args_value から取ってくるだろう、と
• args_value は strcut printf_arg
• これが pa_pointer を持ってる
• ってことでこいつがポインタっぽいなー
• void * だし
• ちなみに ptr が null だったら (nil) って表示するっぽくて
• ptinrf("%p", NULL);
• ってやると (nil) って出てきた
• やったね
• ptr が NULL じゃなかったら 0x ... って出力してる
• ちなみに full width character とのかねあいなのか、 is_long とかってオプションが
• glibc 2.19 だと is_long = 0 だった
• HEAD だとちゃんと処理が書かれてた
• blame すると 1995年とかのもある
• 2014年現在メンテされてるのすごい
• fspec のはなし
• prosess_arg って macro の引数
• 呼んでるのは vfprintf.c の
• 1635:          process_arg (((struct printf_spec *) NULL));
• 2004:            process_arg ((&specs[nspecs_done]));  
• とか
• たぶん NULL のやつが一番最初の実行。
• nspecs_done のやつは続いてく処理っぽい。
• つまり1引数処理が終わると ++nspecs_done されていく
• specs ってのが struct printf_spec
• それが nspecs 分ある
• その n は割と適当で、32とか決め打ちされてた
• 領域足りなかったらもう一回 alloca とかしてるっぽい
• つまりどういうことだってばよ
• fspecs に alloca して printf_arg が入っていく
• 引数を処理していくと nspecs_done が増えていく

ということで、毎回出力が違うのは alloca したメモリ領域の zero fill されていないゴミの値だろう、という結論に。

つまり前の値が書き変わってなければ同じものが出るんじゃないか、ということで %p を多くしてみる。

そうすると毎回同じ値が出力されるようになりました。
やっぱり確保した領域のゴミっぽいですね

つまり、可変長引数を扱うためにメモリはとりあえず確保しとかないといけなくて、処理した値はそこに入れられる、と。

メモリの値は0にする保証とかは無いので、処理が無ければメモリに入ってた値がそのまま出ちゃう、ということっぽいですね。

書いちゃえばそりゃーそーか、ってなる話なのだけれど、引数があることを想定した段階で関数はその処理を書かざるを得なくて、その処理の副産物みたいなのが垣間見えました。

glibc 読んでてな小ネタ

• リアル : 「ここを消すと動かなくなる」
• printf_arg が、マクロの中で宣言されていなくて外で宣言されていて
•       union printf_arg *args_value;>/* This is not used here but ... */
• とか書かれてました。
• do { ... } while(0)
• なんでこれ括られてるのー、ってなってた
• たぶんスコープが欲しかったんだろう
• でも後から { ... } だけの部分とかあった
• たぶん昔は do 書かないと怒られたんだろう
• バッファが溢れないようにするには
• ポインタを説明する時に size 調べて malloc するか、 char hoge[256] とかやった方が良いのか、って話してた最中
• サイズが足りてなかったら 2倍 alloca する、みたいなルーチンが fspecs のところに
• とりあえず適当に確保して足りなかったら増やせばええんやー、って
• 関数だと思ったらマクロだった
• process_arg ((&specs[nspecs_done]));  
• prosess_arg って関数が無い
• マ、マクロだー
• マクロのメンテって大変なのでは
• printf とかがあるからそりゃ glibc の依存度ヤバいのでは
• というか printf がエンバグしたら全部アカンのでは
• でもメンテしてるのすごい

そんなこんなで気付いたら

3時間ぐらい glibc とかと戦ってました。

このブログも書くのに3時間ぐらい。
いやでもなんだかんだ読んでてこうなるんじゃね、ってのを予想して実行してそれが出た時にはうおーってなりましたまる

最初のポインタについて話をしていは部分は yota さんがまとめてくれたっぽいのであうとそーしんぐ。

ハッカーズチャンプルー 2014 に行ってきた

2014/07/12 にあった ハッカーズチャンプルー2014 に行ってきました。
2013も行ってきたので2回目。今回もカンファレンス + ビーチパーティー 参加でした。

例のごとくとりとめもなく感想を書き続ける。

カンファレンス

全体のプログラムはここなんだけれど、トップなので年ごとに変わってそう。

書いてる段階では無いけれど URL は予想でこうなるんじゃないかなー、とか。

OpenStack なおはなし

OpenStack の詳細分かってないのでなんとなーく聞いてた。

DevOps 的な話なのかもしれないけれど、インフラと開発の狭間って結構大きくなってきたかなー、とか。

Developer は OpenStack 環境があればインフラをぽんぽん立てられそうだけれど、 OpenStack を構築するのは大変そう。その間には大きな狭間がありそうだなー、とか。別に根拠は無くてありそうってイメージ、くらいなのだれど。

あと公式ドキュメントにバグあるとか考えたこと無かったなー、とか。

それを「俺達が踏み抜いてって直してきます」って姿勢すごい。

ウェブ解析士 なおはなし

ウェブ解析士知らなかった。

サービスとかする上でログ解析とかそういったことはやっぱりするのねー、とか。

解析ってどういう手法使ってるのだろう、とか思ったり。何か名前付きで手法化されてりしないのかなー、とか。

コストに見あった成果がありますか、ってのはビジネスでは重要なポイントとかうるさく言われそうだよなー、とかとか。

Data Scientist なおはなし

!= データサイエンティスト。

バズワードっぽいアレでも中の人が詳しく解説してくれるとうれしいなって。

というかデータサイエンティストがアカン感じになったのは組織のマーケティングとか、イメージとかのせいなのかなー、とか。実際何やってるかとかじゃなくて周りがどう見るか的な問題。面倒。

データサイエンティストは、データに携わる人の称号じゃなくて、サイエンティストがなるもんなんですよー、ってのは言われるまで分かんなかった。後者の方が妥当だけれど前者のイメージが多そうだよなー、って。私もそうだったし。

解析にも種類がある、ってのはちょっと乗っかりたい案。厳密なアルゴリズム系のやつと、アドホックな機械学習のやつ。

個人的に機械学習はランダム要素とか入ってくるプログラムなのでなんか趣味が合わないとか思ってて、解析にもそういうランダム要素が無い世界もある、とか言われると少し気になる。いやスパムフィルタとかにも関係あるのかもだけれど。

PostgreSQL なおはなし

PosstgreSQL は拡張しやすいよー、ってところはここまで拡張するのか、とか思った。

データ型定義とか外部言語用のインターフェースが用意されてるとか。

でもDBは標準的な機能しか使ったことが無い(各DB独自機能を使ってない)身からするとDBでそこまでやるのかー、とか。

DBでやった方がパフォーマンスチューニングとかの恩恵があるのかな。

あと、開発コミュニティが盛んっぽい。forkも大量らしい。

そういう意味でも拡張しやすいのかなー、とか。

本家の開発は patch 方式らしくて、 pull request お待ちしてます、とかでは無いみたい。

OSS ごとに文化があるからそれを調べないと、とか誰かがつぶやいてた。Github 使えば良いや、って訳でも無いらしい。これは naoya さんの話にも繋がりそう。

Web の変遷なおはなし

Web の歴史の話から入ったけれど Linux Kernel 2.4 の時代とか分からなかったので、 LAMP 前は分からず。LAMP がギリギリ分かるかどうか、くらいなのでふーむ、とかって聞いてた。

これからの時代はクラウドの外部サービスに委託できるところはしておいた方が自分達のやりたいことできるよー、と。これは次の話にも繋がってそう。

というか紹介している外部サービスめっちゃ多かった。あれってどこで見つけてるんだろう。

とにかく外部サービス入れたら良いわけではなくて、必要な部分入れましょうねー、と。

これは PostgreSQL の話にも繋がってるっぽいなー、とか。自分達のスタイルを見つけましょう的な。 無理して流行りに乗らなくても良いんじゃね的な。

結局バランスっぽい。むずかしい。

これからのエンジニアなおはなし

枯れた技術の水平思考っぽい話なのかな。

4K なんてユーザはうれしいのかー、みたいな。

ユーザ視点で考えてビジネスしようぜー、みたいな。

あと視野狭いとやばいよー、とか。

少子高齢化なんて日本だけだぜー、とか。

感想書いてて思ったけれど割とバッドノウハウから学ぼう、って感じなのかも。

Azure なおはなし

「とつぜんのくらうでぃあさん」

Azure こんなだぜー、って感じ。対比はやっぱり某密林社なのか。

そのあたり使ってないので差分が分かんなかった。

あと開発プラットフォームのサポートとか言語サポートとかが当然のごとくついてるのはすごいよなー、とか。その情報源はタイムラインだけれど。

100万台仮想マシンがー、とか規模がー、とか。

ものづくりマインド + 女性エンジニア なおはなし

ゲームな業界から参戦なさってた。女性エンジニア率が低いのは同じらしくて、継続率も低い。結婚とか出産とかのイベントがあると続けづらいよ、とのこと。その辺りは周りの理解だよなー、とかつくづく。

Jenkins さんはゲーム業界でも仕事してるらしい。やっぱり適材適所で入れてくのが良いっぽいかー。

あとエンジニアのマインドの話。

「泣くな。いやたまに泣いちゃいそうになるの見たことあるけれど。というか泣くならトイレで泣け。」

とのこと。つよい。「母は強し」感ある。

技術についてけないよー、とかもついてけば良いし、ヤバいってなったら会社やめたら良いし、世の中案外そんな感じなのかもしれない。とか言えたら大丈夫なのだろうけれど。

あと学生特権でお弁当頂きました。ごちそうさまです。

ビーチパーティー

学生料金でタダ飯でした。こちらもごちそうさまです。

結構書いたのでこの辺りからアバウトで。

仕事は東京でするか沖縄でするかー、とかリモートワークーがー、とかとか。仕事っぽい話は割と実感なさげ。

あとは英語喋れると外国人エンジニアからしょーもない話からここだけの話まで聞けます、とか。

話は聞けるわ飯は食えるわのイベントでした。

というかみんなこようよ、とかどことなくつぶやく。

台風などありましたが運営の方々お疲れ様でした + ありがとうございました。