ProofSummit 2011 で『CoqによるMsgPackシリアライザの証明と実装』という話をしました。

ProofSummit2011でMsgPackを証明したときの話をしてきました。内容は名古屋Reject会議で話したことを膨らませた感じになっています。
話の趣旨としては「バグって怖いじゃん → じゃあ証明しようぜ → やってみた」みたいな感じです。

スライド

CoqによるMsgPackの証明
View more presentations from Hiroki Mizuno

ustream

http://www.ustream.tv/recorded/17493318

感想

  • 新宿ダンジョンこわい
  • [twitter:@ikegami__]さんと[twitter:@masahiro_sakai]さんにAgdaを教えてもらえたので、とてもよかった
  • Software Foundationsの和訳プロジェクト、気になります

gitとRedmineと連携させるgitサブコマンド: git-ticket

git + Redmineで開発する場合、Redmineのチケットごとにトピックブランチを切ることが多いですが、ちょいちょいチケットの内容を忘れてしまいます。 そういうときに、いちいちブラウザでチケットを見にいくのがダルいので、チケットのサマリを表示するgitのサブコマンドを作りました。
なお、本コマンドはbleis-hooksと併用することを想定しています。

インストール方法

git ticket subcommand · GitHub からダウンロードし、パスの通ったディレクトリに配置してください。

$ wget https://raw.github.com/gist/014371584dbf85d053ed/f8ade6f7fc36a4c8f49f72a538a6322bfb726bf8/git-ticket
$ mv git-ticket /path/to/some/dir
$ chmod a+x /path/to/some/dir/git-ticket

Ruby1.8の場合は、json gemのインストールしてください。

$ gem install json
$ export RUBYOPT=rubygems

初期設定

redmineのURLとapikeyを設定してください。

$ git config --global redmine.url https://example.com/redmine/
$ git config --global redmine.apikey some_api_key

使用例

登録されているチケット


1) git ticket <チケット番号>

id/<チケット番号>というトピックブランチを作成し、チケットのサマリを表示します。

$ git ticket 701
Switched to a new branch 'id/701'
Author: Ban Jun
Date:   2011/08/06 21:51:13 +0900

iPhoneアプリに戻るボタンとリロードボタンをつける
#693 関連
2) git ticket

トピックブランチにいる場合、対応するチケットのサマリを表示します。

$ git ticket
Author: Ban Jun
Date:   2011/08/06 21:51:13 +0900

iPhoneアプリに戻るボタンとリロードボタンをつける
#693 関連

似ているもの

ﾊﾟｸｯﾃﾅｲﾖ

Jenkinsのビルド結果をリアルタイム通知するプラグイン『Jenkins Websocket Notifier』を作りました

追記: 公式プラグインになりました。Websocket Plugin - Jenkins - Jenkins Wiki

「pollingが許されるのは小学生までだよねー キモーイ キャハハハハハハ」というわけでビルド結果をpush通知するJenkinsプラグインを書きました。

特徴

  • Jenkinsのビルド結果をWebsocketを使って通知します。
  • モダンなブラウザはWebsocketに対応しているので、Javascriptで簡単に通知を受け取れます。
  • Websocketはプラットフォームに依存しないプロトコルなので、Javascript以外でも通知を受け取れます。

インストール方法

  1. https://github.com/mzp/unageel/archives/master からwsnotifier.hpiをダウンロードする。
  2. wsnotifier.hpiをJenkins の管理 > プラグインの管理 > 高度な設定 > プラグインのアップロード からアップロードする。
  3. Jenkins の管理 > プラグインの管理からWebsocket Pluginをインストールする。
  4. Jenkinsを再起動する。

設定方法

Jenkins の管理 > システムの設定 > Websocket Notifier で Websocketサーバを起動するポート番号を指定します。

(プロジェクト名) > 設定 > ビルド後の処理 でWebsocket Notifierのチェックボックスをオンにします。


利用例 その1: Chromeエクステンション

Jenkins のビルド結果を通知する Chrome エクステンション作った - mallowlabsの備忘録 を改造して、Websocket Notifierに対応させました。 使い方・機能は変っていませんが、通知速度が格段にあがっています。
パッチはすでに本体に取り込まれているので、インストール方法等はリンク先を参照してください。

利用例 その2: iPad/iPhoneのXFD化

WebsocketはJavascriptで簡単に扱えるので、ビルド結果によって背景色を切り替えるWebページも簡単に作れます。これをiPad/iPhoneで表示すれば、iPad/iPhoneテスト結果を通知するXFD(eXtream Feedback Device)として利用できます。

<html>
  <body bgcolor="red" id="bg">
    <script>
      var elem = document.getElementById('bg');
      var ws = new WebSocket('ws://localhost:8081/jenkins');
      ws.onmessage = function(msg) {
          eval('var obj = ' + msg.data);
          if(obj.result == 'SUCCESS'){
              elem.bgColor = 'green';
          }else{
              elem.bgColor = 'red';
          }
      };
    </script>
  </body>
</html>

http://github.com/mzp/unageel/blob/master/xfd.html

利用例 その3:ダンボーのXFD化

上記の応用でビルド結果に応じてダンボーの目の色を変えることができます。
ダンボー本体はよつばとリボルテック リボルテックダンボーを、目の色の制御にはArduinoをはじめようキットを使っています。 目には大須で買ってきたフルカラーLEDを仕込んでいます。

技術的な話

  • ws://localhost:8081/jenkins に接続するとJSON形式でビルド結果が飛んできます。
  • ポート番号は設定によって変更可能です。
  • ビルド結果は{ "name" : "test", "result" : "success", "number" : 1 }のような形式です。

お礼

ゆるい勉強会の開き方

DSC_0960.JPG

@akinekoさんの勉強会を開催or参加する人が気をつけたい11のこと - Akinekoの日記に影響されて、ボクが勉強会を開くときに気をつけてることを書いてみます。

いままでにやった勉強会

勉強会の方針

気楽に開催できて、気軽に参加できるゆるい勉強会を目指しています。
なので双方の負荷を減らすためにお金をあまりかけないようにしています。

勉強会のテーマの決め方

思いついたらTwitterに投げて、そこそこの反応あったら開催してます。 だいたい3fav/RTぐらいを目安にしています。
他の勉強会の懇親会で盛り上って開催することも多いです。

募集サイト

partake.inがお気に入りです。

お気に入りポイントは

  • 登録にTwitterアカウントが必須なので、連絡がとりやすい
  • 共同編集者が設定できるので、一人に負荷が集中しない。
  • Twitterに告知を投げるボタンがあるので簡単に宣伝tweetを投げれる。
  • 開催日前日に自動でリマンダをDMで送ってくれる機能がある。

です。

会場選び

なるべくお金をかけたくないので、勉強会用に無料で会議室を貸してくれる企業さんや安く借りれる公共施設を利用しています。 ニューキャストさんにはお世話になりっぱなしです。

公共施設を借りる場合はプロジェクターやネットワーク環境が基本的に無いので、自前で準備する必要があります。 ネットワーク環境はたいていの人が持っていますし、プロジェクターも意外と持っている人が多いので事前にお願いしておけばなんとかなることが多いです。

どうしても高い会場を借りないといけない場合は、参加費をいただいています。定員の8割程度が参加してもらえれば元がとれる程度の値段設定にしています。

発表者交渉

募集ベージに「発表希望者は@mzpまでreplyを!」と書きはしますが、それほどreplyは飛んできません。
ただ、こちらからお願いすれば話してくれる人が多いので、知り合いや参加者に直接お願いしています。
発表者には募集ページの編集権限を渡してしまって、適宜発表タイトルなどを修正してもらうようにしています。

参加者への連絡

ごめんなさい、ほとんどしてません m(_ _)m。partakeのリマインダ機能にまかせっきりです。

懇親会

キャンセルに怯えたくないので、実施してません。
店の目処だけをつけておいて、当日、希望者を確認してその場で手配するようにしてます。

会計

お金をかけていないので特にやってません。

参加登録について

参加者が少ないと参加登録をためらう人が多いので、気軽に参加登録してもらえると助かります。
予定が微妙な人は"仮参加"でも十分でもOKです。

キャンセル

なるべく多くの人に参加してもらいたいので、無理になった時点でキャンセルしてもらえると助かります。
当日キャンセルは状況次第ですが、たいていの場合は気にしていません。

今後の課題

  • 参加者の人数が読めるようになりたい。
  • ustreamをできるようになりたい。ustream専用PCがいるかも。
  • 初参加者のフォローがあまりできてないので、できるようになりたい。

「ActionScriptを使わないswf勉強会 #1」を開催しました

東京で「partake.in」を主催してきました。「東京の勉強会にも一度は参加したいなー」と前から思ってましたが、まさか主催することになるとは思ってませんでした。会場の手配等々は@7shiさんに頼りっぱなしでした。ありがとうございます。

「Flashのバイナリを直接いじりましょう」というよく分からない趣旨でしたが、結果として30人以上の人が集りました。さすが東京はすごいですね。

どういう人が集まるのか想定できていませんでしたが、携帯ゲーム業界の方がわりといりゃっしゃってた気がします。

発表資料まとめ

もっといいまとめ

感想(140文字程度で)

  • 普段は聞けない話というか、知りもしなかった話がいっぱい聞けて楽しかったです。
  • Flashの勉強会は女子率が高いと聞いていましたがデマでした。
  • どの会社にも一人はFlash Lite 1.1を動的生成する係がいるらしい。二人はいない。
  • 今熱いのはJavascriptによるFlash Playerの再実装らしい。そんなバカな。
  • 懇親会で食べた焼き肉がたいへんおいしかったです。

MessagePack for OCamlを公開しました

くえにしさん([twitter:@kuenishi]さん)に誘われたのでMessagePackハッカソンに参加してきました。
MessagePack本体のレポジトリにMessagePack for OCamlを取り込んでもらったので、みんな使ってください!

MessagePackって?

JSONやYAMLと同程度の表現能力をもった省スペースなオブジェクトシリアライザです。対応言語もC/C++/Java/D/Ruby/Haskellなどと非常に多いです。 対応言語言一覧 → http://wiki.msgpack.org/display/MSGPACK/QuickStart

公式Wikiの採用実績によると、かなりメジャーなプロジェクトも採用されているようです。実際、ハッカソンにも仕事で利用されている方が結構来ていました。

実はボクたちの作っているチャットアプリのAsakusaSatelliteでもちょっとだけ使ってます。

MessagePack for OCamlを作りました

「OCamlだってMessagePackを使いたい!」というわけで、OCaml版を作りました。
現状ではシリアライザ・デシリアライザ部分のみです。 RPCは今後の課題です。

インストール方法・使い方

http://wiki.msgpack.org/display/MSGPACK/QuickStart+for+OCamlに書いたので、そちらをご覧ください。
API リファレンスもあります。

実装方法


変換処理といえば証明駆動でしょ、というわけでコア部分はCoqで証明されています。
このとき苦労したことはReject会議のスライドに書いてあるので、興味のある方はどうぞ。

なお、Coqで生成されたコードもレポジトリに入っているので、普通に使う分には意識する必要はありません。

今後の課題

  • 効率が悪い: Coqと連携させる関係で1バイトがboolの8項タプルで表現されて、効率的には微妙な気がしています。誰かに怒られるか、自分が困ったら考えます。
  • RPCがない : IDL処理系ができたら本気だします。

ハッカソンの感想

  • たのしかったです! さそっていただいて、ありがとうございます!
  • 「仕事でMessagePackを使ってます/使いたいです!」みたいなパワフルな人たちばかりで、すごかったです。
  • 型によって処理を変えれる言語だと便利なシリアライザが作れていいなぁ
  • [twitter:@frsyuki]さんと[twitter:@nobu_k]さんがIDLの仕様をどうするかの議論をしていたので、ちょっと参加させていただきました。「それ、OCamlだとちょっと....」みたいなことしか言ってなかった気がしますが。
  • 複数の言語で便利に使えるIDL仕様を決めるのは、なかなかスリリングな作業で楽しかったです。
  • 結果としてなかなかいいIDLの仕様を決めれたので、処理系が楽しみです!

おまけ

東大こわい