ITSP PBL で作ったもの・使った技術やツール

PBLというチーム開発の授業でうちのチームはこんなの作ったり使ったりしたよという記事です。 成果発表会や展覧会では技術的なことの説明はほとんどしなかったように思うので、せっかくなので公開しておきます。

来年以降この授業を取る人の参考になればと思います。

(他のチームのも読みたいので誰か書いてください！)

ITSP について

東工大のIT特別教育研究コースのことで、このコース専用の授業がいくつかあったりします。

例えば、

• ソフトウェア開発演習
  • Android アプリを作ってみる演習。自分は ProveEverywhere という Android で Coq の証明を書けるアプリを作った
• ソフトウェアテスト演習
• システム検証基礎演習
  • Alloy を使った形式検証の演習
• PBL (後述)

などがあります。わりと実践的なものが多いです。

PBL について

ITSP コースのメインが PBL (Project Based Learning) という授業です。単にITSPといったときはこのPBLを指すこともあります。

PBLは4月から12月の展覧会に向けてチームで企画から開発までやってみるという授業です。

授業で習うことはほとんど上流工程のことやコミュニケーションについてで、具体的な開発についてのことはまったくやりません。各チームに完全に任せられる感じになります。

僕達のチーム (White Chocolate、以下白チョコ) は7人 (+2人、読めばわかる) でした。他のチームは人数が減っていったりしたのですが、白チョコは誰も欠けることなく最後までいきました。

使ったサービス

GitHub

ソースコードの管理は GitHub の教育用 organization を使って無料で10個プライベートリポジトリをもらって使っていました。現在10/10使っています。

申請に2,3回はねられたのですが直接メールを送ったらすぐに受理してくれたので、拒否されたらすぐにメールを送ってみるといいと思います。

白チョコの organization

idobata.io

チーム内のチャットツールとして、idobata.io を使いました。 チャットツールは他にもいろいろありますが、無料で、かつ他のサービスと連携しやすいこれを選びました。

今ならデファクトっぽくなっている Slack を選ぶかなと思います。 当時 Slack にしなかった理由は、無料の範囲だと10000件しかメッセージを保持しなかったのと外部サービス連携が3つまでだったからです。今はどうか知りませんが2014年4月時点ではそうでした。当時は10000件以上前のメッセージを検索することもあるかなと思って Slack はやめたのですが、結局メッセージを検索することはしなかったので Slack のほうが今っぽいしいいかなと思います。外部サービスもちょうど3つ (GitHub, Wercker, Heroku) だったので Slack でよかったです。

あと idobata.io の Chrome 拡張めっちゃ便利でした。

Heroku

チャットに住まわせる Hubot を Heroku で動かしていました。デフォルトでは死なないように何分かごとに ping が飛んでくるのですが、それでもときどき死んでしまうので困りました。

Wercker

CI サービスは Wercker を使いました。Wercker にした理由は、プライベートリポジトリでも無料でOKだったのと、自前で環境を作れるからです。今回 Play を使ったので、wercker-box-activator という環境を作って使っていました。

mackerel

サーバの負荷を見るために使っていました。

Google Drive

仕様書以外の文書等はここで管理していました。

作ったもの

Yukiho

https://github.com/white-chocolate/yukiho

チャットに住んでいる bot さんです。ラブライブ！の高坂雪穂さんがモデルです。白チョコが崩壊せずうまくいったのはこの子がいたからと言っても過言ではない気がします。

(経緯)

Yukiho は優秀でいろいろやってくれます。

ラブライブ！の放送をリマインドしてくれる

by tondol

素数を見つけると教えてくれる

by tokuhisa

東工大っぽさ

ラブライブという単語を見つけるとラブライブ！のGIFを貼ってくれる

by amutake

animate me ラブライブ の alias です

寿司, 鮨, スシ, すし, sushi, (寿司の絵文字) という単語を見つけると寿司ゆきの画像をランダムに貼ってくれる

by amutake

Qiita の bot のパクリ (https://twitter.com/mizchi/status/535731282869616640)

ランダムレビュワー

by amutake

https://github.com/white-chocolate/yukiho-reviewer-lotto

sakatam/hubot-reviewer-lotto を folk して改造したもの。

deploy to production

by amutake

bot に頼むと GitHub にプルリクを送ってくれてマージすればデプロイされるあれです。 Atrae Tech Blog — Hubotとwerckerを利用したデプロイフロー改善 を参考に作りました。

ARISA

チームで作った Web サービスです。名前は Academic Research Investigation Service by Association の略です。(ラブライブ！の絢瀬亜里沙さんがモデルという噂がたっていますが...)

PBL は一応 Android アプリを作るという授業になっていますが、授業に沿って企画したアプリがモバイルアプリではなくPCから使えたほうがいいようなものになってしまったので先生に確認したところ、EC2 使うならいいよということでしたので Web サービスになりました。

サービスの内容は、論文に対してコメントとか質問とかをつけることができるというものになっています。

また、ある学術分野 (キーワード) から近い分野を視覚的に表示してくれる分野マップというものもあります。

サーバとクライアントは Web API (JSON) 経由で情報をやりとりしています。API サーバは Scala + Play framework + MySQL (Slick) + Elasticsearch (elastic4s) で動いていて、クライアント側は JavaScript + Vue.js + page.js + D3.js で動いています。

Scala を使ったのはよかったのか悪かったのかわからないです。もちろん自分は慣れてるのでいいんですが、他のメンバーは全員 Scala (や他の関数型プログラミング言語) の経験は全くなく、最初はみんな Scala わからない〜〜という感じでした。でもみんな普通に書けていたのでいいのかな…。いずれにしてもみんなが慣れるまではもう少しサポートすべきだった気がします。

また、サーバはひとつしか使えなかった (m1.small) ので、API サーバも静的ファイルサーバも MySQL も Elasticsearch も論文メタデータクローラも類似度計算も全部一つのサーバで動かしていました。途中から重すぎて自分の VPS (お名前VPS2Gプラン。m1.small よりはいい…)に移行しました。

あと Nginx を前にたててリバースプロキシにしてました。

Scala bindings for Microsoft Academic

by amutake

ARISA では論文メタデータを収集するために、Microsoft Academic という Microsoft が提供している論文データベースを使っています。これはその API を Scala から便利に利用するためのライブラリです。 dispatch というライブラリを使っています。

Microsoft Academic Metadata Crawler

by amutake

Microsoft Academic から論文のメタデータをとってきてDBに保存するプログラムです。上の自前ライブラリを使っています。

Calculation Similarity

by tamaizumi

キーワード間の類似度を計算するプログラムです。同じ論文の二つのキーワードは近い、引用・被引用の関係にある論文についている二つのキーワードはわりと近い、というように計算しています。

これは事前に計算しておいて分野マップのところで使っています。

Scala 製。

データを Elasticsearch にぶちこむやつ

DBに保存してある論文メタデータを Elasticsearch に入れるやつです。 今だったら embulk とか使えば良さそうです。

Ruby 製。

やりたいけどまだできてないこと

クラウドっぽくなるならインスタンスもっと使ってもいいよという先生の言質をとった (先生が酔ってたときに) ので、Spark とか使って類似度計算を一気に行いたいなあと思っているのですがまだできていません。

あと Microsoft Academic 以外の論文データベースにも対応させたり、最終的には自前で論文データベースを作ったりしたいです。

今後どうするか

発表するといろいろな人から今後どうするか聞かれるのですが、それはまだ未定です。チームで話し合って決めたいと思います。

その他

チームの順位

5チーム中1位でした。

進捗報告

だいたい週一で集まって進捗報告をしていました。夏休み中もやっていました。

勉強会

比較的早い段階で、Yukiho を開発するための Git 勉強会と、Scala の勉強会を開きました。 Scala の勉強会は自分の説明下手のせいで良かったのかはわかりません...

親睦会

ITエンジニアといえば寿司、みたいなところがありますが、ちょうど自分が寿司を握れるので自分たちのチームでも寿司パーティを開いて親睦を深めました。

寿司のプロ #w8sushi pic.twitter.com/9Z1bquJZlN

— しゃも/Tokuhisa,Fumiaki (@tokuhisa_f) November 19, 2014

匠による🍣講習会 #w8sushi pic.twitter.com/gLrIFeBbhi

— とんどる (@tondol) November 19, 2014

その他にもチームでラブライブ！の聖地巡礼したり映画館に楽園追放を見に行ったりしました。

おわり。

(第二回)更新を楽しみにしているWeb漫画10

個人的に更新を楽しみにしているWeb漫画10の2回目です。前回と被っているものもあります。 Web漫画とは言えないものもありますが、とりあえず2015年2月3日現在Webで読めればよしとします。

(順不同)

• NOBELU-演-
  • 一番楽しみにしてる
• 宇宙大恋愛
• マイアニマル
• 天沢君とカムナちゃん
• DRAGON BALL 魔人ブウ編
• Helck
  • ピウイがかわいすぎてつらい
• ReLIFE
• ポチクロ
• 市場クロガネは稼ぎたい
• 猫なのでもうすぐ死にます
  • おとうさん(ねこ)かわいいのでもうちょっと出してほしい…

有名なやつばっかりでごめんなさい。でも有名になる漫画やちゃんと編集の人？がついていそうな漫画はやっぱり面白いです。

--

自分はいつも webcomics.jp というサイトで更新を確認しています。

自分のリストはこんなかんじです。

Keycastr と Gifzo が便利だった

utop のバグっぽいものを見つけたので、それを issue に書くために GIF のツールを使ってみた。

keycastr/keycastr · GitHub

Gifzo - 宇宙一簡単なスクリーンキャスト共有

Keycastr はキーストロークを画面に表示してくれるツールで、Gifzo はスクリーンショットを撮るように GIF を作って共有できるツール。(Gifzo は Gyazo GIF になったっぽいけど、Gifzo のほうが始めるタイミングと終わるタイミングを自分で決めることができてよかった。たぶん Gyazo GIF でも設定すれば出来るんだろうけど調べてない。)

$ brew cask install keycastr gifzo

でインストールできる。

keycastr の方は更に設定が必要で、

のところにアプリケーションをドラッグ&ドロップする。(Mavericks と Yosemite だけかも)

これで下みたいな感じの GIF をとってバグ報告した。

Frama-C のインストールメモ

• 環境: OSX Yosemite
• パッケージマネージャ: homebrew, homebrew-cask, opam
• コンパイラ: ocaml4.01.0+clang-fix

1. brew cask install xquartz
   • これを入れないと pkg-config でコケる (X が入ってないというエラーはでない)
   • 普通に XQuartz.dmg を入れた状態だとダメだった
2. brew install pkg-config gtk+ gtksourceview libgnomecanvas libgnomecanvasmm
   • ここらへんは try and error でやってたので何が必要で何が必要でないかはわからない
3. opam install frama-c

CodinGame をやってみた

面白そうなのでやってみました。

いくつか解いてみた感想

• ただのプログラミングコンテストの問題
  • 標準入力から情報を受け取って、なんらかの計算をして標準出力に計算結果を出力する類の問題
  • 問題のテストケースをゲームっぽくグラフィカルに表示するだけ
• 入力が何を意味しているのかや、どんな出力をすればいいのかがわかりづらい
  • 普通のプロコンの問題であるような、入力と出力の例がない
  • 動かしてみながら把握するしかない
  • これに時間がかかってしまう
• いろんな言語が使えるのは良い
  • ghc のバージョンは 7.4 だった
• なんかもっとゲームっぽいインタラクティブな何かがあるのかと思ったけど違った

追記

入力の意味やどんな結果になればいいかはゲーム画面(左上のウィンドウ)を下にスクロールしたら書いてありました……。

チャットでも証明が書きたい

チャット上で証明が書けたら面白そうだなと思ったので、ProveEverywhere のサーバを使う hubot スクリプトを書きました。

こんなかんじ。

導入方法

(hubot 自体の導入方法については他の記事に任せます)

1. 適当なサーバに Coq 8.4 以上をインストールします。
2. prove-everywhere-server を Coq をインストールしたサーバにインストールして起動します。
3. hubot の package.json の依存ライブラリに hubot-prove-everywhere を追加します。
4. hubot の external-scripts.json に "hubot-prove-everywhere" を追加します。
5. 環境変数 HUBOT_PROVE_EVERYWHERE_URL に prove-everywhere-server が動いてるURLをセットします。
6. hubot を起動します。

使い方

new

hubot proof new とすると、新しい coqtop が起動します。表示されるIDがそのIDです。

put ID SCRIPT

指定したIDの coqtop に script を入力します。

例えば hubot proof put 3 Goal forall P Q : Prop, (P -> Q) -> P -> Q. とすると、IDが3の coqtop に Goal forall P Q : Prop, (P -> Q) -> P -> Q. を入力します。

必ず . で終わるようにしてください。

証明の状態を戻したいときは Back 1. などを使ってください。

terminate ID

指定したIDの coqtop を終了します。

なつやすみのにっき

夏休みです。

Coq Summer School

8月の終わりに NII Shonan School on Coq に行ってきました。

一週間みっちりCoq漬けでした。楽しかった。でも英語ができればもっと……。

夏ゼミ

Coq合宿が終わった3日後から2泊3日の研究室合宿がありました。千葉の館山に行きました。

1,2日目はずっとゼミでした。ものすごく疲れた。自分は Coq School でどんなことを学んできたかについて発表しました。

最終日はみんなで鋸山に行きました。

下の写真は帰りのフェリー。予想以上に良かった。また乗りたい。

幹事として至らないところもありましたが無事に終わって良かったです。ありがとうございました。

あと酔った同期がめちゃくちゃおもしろかったです。普段もあんな感じでいればいいのに……。

ProofSummit2014 & JSSST2014

夏ゼミの3日後から名古屋でした。ProofSummit -> Coq/SSReflect チュートリアル -> JSSST という順番。

ProofSummit

ProofSummit2014でLTをしました。 内容は ProveEverywhere についての宣伝です。

ProveEverywhere というのは僕が Android アプリを作る授業で作ったアプリで、CoqIDE を真似たものです。

Coq をスマホで動かすアプリはいくつかありますが、それらは Coq をアプリにまるごと入れています。これは coqtop サーバを別に用意するので軽かったりします。

(この発表の時点ではリポジトリは https://github.com/amutake/prove-everywhere にあったのですが、関係するディレクトリとかリポジトリが増えてきたので https://github.com/prove-everywhere に移行しました)

Coq/SSReflect チュートリアル

Affeldt さんによる Coq と SSReflect/MathComp のチュートリアルです。

正直、誰でもわかるような簡単で、ちょっと触ったことがある人なら退屈な内容になるんだろうな〜と思っていましたが、全くそんなことはなかったです。とても濃いチュートリアルでした。

この資料 (https://staff.aist.go.jp/reynald.affeldt/ssrcoq/) は全 Coq ユーザーが読むべきだと思います。

JSSST

日本ソフトウェア科学会の全国大会です。最終日の Coq セッション (Coq のみのセッション!!) で発表しました。

外で研究について発表するのはこれが初めてだったのでものすごく緊張しましたが、無事に(？)終わって良かったです。

いま

今は BIGCHA というのに参加しています。Hadoop を使ってなんかアプリを作ろうというやつです。言語は30億のデバイスで走るという噂のジャバです。

ジャバのコードを見ていると頭が痛くなる病気になってしまいました。

おわり

おわり。

追記

今気づいたけど BIGCHA 以外すべて Coq 関係だった