600000007

プログラムと折り紙のブログです。

JJUG CCC 後日談

社内にて

今回は初めて同僚をJJUG CCCに誘ってみました。
その結果、後輩が一人参加してくれて、会場を右往左往する姿を見ることができました。

そして後日、週一で行っている社内勉強会にて実際に見たセッションを紹介することになりました。
私と後輩で交互に発表。ひとり7分。他人の資料でLTをやるような奇妙なイベントになりましたが、勉強会の同志の意識を高くすることには成功したようで、Java Puzzlersの購入(会社のお金)が決定しました。

Jenkinsと

当日の懇親会でJenkins作者の川口さんとお話をすることができました。
できました、というか酔っ払って絡みました。申し訳ございません。

その場にて熱い想いと酒臭い息をぶつけてしまい、
「スレーブをWindowsサービス化するために.Net Framework3をインストールしないといけないのめんどくさいんです」
.Net Framework2でビルドしてれば問題ないのかと思ってました」
「確か互換性がなくて・・・どうすべきか調べてご報告します!」
と約束をしてしまいました。

してしまいました、というよりは約束したかったんです。Jenkinsに関わりたかったんです。
その後Jenkinsのコードとissueとプルリクとドキュメントを読み漁った結果、このプルリクがマージされれば.Net Framework3のインストールが不要になることが判明。
川口さんにその旨連絡したところ、マージしていただけました。万歳。

Ant「ビルドできません」Travis「よし通れ」

色々順番を間違ってる気がしますが、人生初LTでした。
初LTはJJUGのビール片手にLT&納涼会でやりたいと思っていたので、実現して嬉しかったです。
運営の皆様お世話になりました。

www.slideshare.net

LTで言えなかった事

  • PRを待ってくれてる感じがした
  • 英語は皆雑だった
    • native同士じゃないから気にするだけ損

LTをやってみた感想

  • 予想外のところで笑ってもらって新鮮だった
  • 終了後に知らない人から話しかけられて嬉しかった
  • 死ぬ程緊張したんだけどこれを平然と何度もやってる人達の神経は信じられない
  • 最前列でうんうんうなずきながら話を聞いてくれた某氏に救われた
  • プロジェクターの闇は深い

Macでssreflect

以下はssreflectをMacで動かそうとした悪戦苦闘の記録です。
最終的には、以下のような構成になりました。

  • Mac OS X 10.9.4
  • Emacs 24.3.1
  • ProofGeneral4.2
  • Coq8.4pl4
  • ssreflect1.5

CoqIDE or ProofGeneral

Mac OS X 10.9では、CoqIDE8.4は起動できません。既知の問題みたいです。
操作性も含めてEmacs + ProofGeneralの構成をお勧めします。

Emacs

デフォルトで入っているemacsや、homebrewでインストールしたものをターミナルで使用すると、なぜかgotoによるコンパイル(カーソルがある位置までコンパイルしてくれる)ショートカットが使えませんでした。
Ctrl + C , Enterを実行すると、C-c RET undefinedというエラーになります。
Emacs for Mac OS X なら大丈夫でした。
これはEmacs.appとしてインストールされます。

ssreflectのインストール

homebrewでインストールします。事前にXQuartzのインストールが必要です。
また、ssreflectのダウンロードパスが変わっているので、brew updateを必ずしておいた方が良いです(していなかったせいではまりました・・・)。
# brew update
# sudo brew install ssreflect

clangエラー

初っぱなからclangエラーでつまづきました。
こちら によると、clangのバージョンによる問題だそうです。
xcode5.0.2にダウングレードして回避しました。

ProofGeneralのインストール

ProofGeneralの最新版は4.2ですが、Emacs24系には対応していません。
そのためmakeに失敗すると思いますが、こちらにあった方法で回避できました。Emacs.appの指定方法もこちらにあります。

あとはProofGeneralにssleflectを認識させる必要があります。
Coq/SSReflectの設定にあるようにEmacsの設定変更をするのですが、homebrewとEmacs.appを使ってる関係上、微妙に異なります。

Emacs.appの設定

~/.emacs.d/init.pl を編集します。

ssreflectの場所

パスは/usr/local/Cellar/ssreflect/1.5/lib/coq/user-contrib/Ssreflectになります。

(setq coq-prog-args
(https://staff.aist.go.jp/reynald.affeldt/ssrcoq/install.htmlcons "-R" (cons "/usr/local/Cellar/ssreflect/1.5/lib/coq/user-contrib/Ssreflect" (cons "Ssreflect"
(cons "-emacs" nil)))))

coq topが見つからない

ProofGeneralが正しくインストールされていると、*.vファイルをEmacsで開けば起動されます。
無事起動したので一安心していたら、

Searching for program: No such file or directory, coq top 

というエラーでコンパイルが進みませんでした。
こちら の方法で回避できました。

ここまでくればちゃんと動くはずです!
こちらばっかですね。インターネット万歳。
mathcompはまだコンパイルが終わらないのでまた今度。

プログラマーは定理証明支援系を勉強すべきか?

定理証明支援って何?

最近、定理証明支援に関連するニュースがいくつか飛び込んできました。あるときはOpenSSLのバグを見つけ、あるときは数学の問題を解決しています。
それらに共通する定理証明支援とは何かを簡単に説明します。

定理証明支援の「定理」「証明」とは、いわゆる数学的なそれを指します。
通常の証明は、人が書き、人が読み、人が正しさを判定します。
定理証明支援系では、人が証明をプログラムとして書き、コンピューターが読み、コンピュータが正しさを判定します。
どうやってコンピュータが正しさを確認するのか?を説明するには余白が足りないので割愛しますが、学校で習ったあの数学の証明を、コンピュータが正しいかどうか判定することが可能なのです。
そしてさらに、その証明を書く作業を様々なアプローチで助けてくれます。

何に役に立つの?

定理証明はプログラムの品質保証に役立ちます。
プログラムの仕様を定理として記述し、その正確さを確認し、正確さが保証されたプログラムを出力することができるのです。
例えばリストを変換する関数を作り、その関数が満たすべき性質を定理として記述します。
ここでは変換後のリストの長さが必ず10以下になる、という定理だったとすると、もしその定理が証明できれば、その関数はその性質を保証されます。
そしてその性質を持った関数をプログラムで使用することができるのです。

今すぐ全てのIT企業に導入すべき?

全てのIT企業が導入し活用するのは現実的ではないでしょう。

理由の一つは難易度です。
定理証明はやはり難しく、プログラミングとはまた別のスキルセットが必要になります。

証明の能力は、自分で証明を書く能力と、証明を読む能力に分ける事ができます。
両者には難易度に大きな差があり、前者は圧倒的に難しいです。

また定理を自分で作る、という行為も難題です。
そのため普段プログラムのテストを書くように、コンスタントに証明を書くというのは想像ができません。

そしてわざわざ定理を書かなくても、簡単なテストで十分な品質を得る事ができるケースも多くあります。

勉強すべき?

すべきだと思います。
自分自身がゴリゴリ証明を書いて活用する事はなくても、誰かが証明したプログラムを使うのが当たり前になるのはそう遠い未来ではなさそうです。
そのときに、何が証明されているのか?何が保証されているのか?を正しく理解する事は非常に重要です。
それらを理解するためには、定理証明で何ができるかを理解している必要があります。
既に証明付きコンパイラも登場しています。

勉強したら数学力は上がるの?

あがりません。
数学力をあげたければ、数学を勉強しましょう。

JarファイルからManifestを読む

意外と手こずったのでメモ。
特定のJarのManifestを読む方法です。
単にMETA-INF/MANIFEST.MF をリソースとして読もうとするだけだと、classpathが通っている他のJarからも探してしまいうまく行きませんでした。
以下は呼び出しているクラスを保持しているJarのManifestファイルを読み込んでいます。

Java1.7で確認済み。

Gradle初心者がはまったこと、悩んだ事。

ここ2週間程、プロジェクトのビルド環境を再整理していてGradleをがっつり触りました。
GradleもGroovyも初めてだったのですが、最初は慣れなくて苦労しました。
その代わりGradle脳になってしまえば非常に簡潔に分かりやすく書けて良いですね。素敵です。

以下の内容はGradel 1.8を前提としています。

タスクに複数の依存関係を設定する

タスクのリストをそのままdependsOnに渡す事ができます。

task copyHoge(type: Copy, dependsOn: ['jar', 'copyBat']) {
    from 'nanikashira'
    into 'dokokashira'
}

タスクに変数を渡す

できません。
その代わりgradleコマンドの引数、タスクルール、動的タスク作成などで代用できます。
私の場合は一部の値が違うタスクを何個か作りたかっただけだったので、動的タスク作成を使いました。

['file1', 'file2'].each { def fileName ->
    task "copyFile$fileName" (type: Copy) {
        from 'nanikashira/$fileName'
        into 'dokokashira'
    }
}

task copyFile(dependsOn: tasks.matching { Task task -> task.name.startsWith("copyFile")})

タスクの中で他のタスクを呼ぶ

できません。
依存関係でタスクをチェインさせる形か、メソッドを書く形などに変形して代用しました。

testで1件でも失敗があるとビルド失敗になってしまう

ignoreFailuresをtrueに変更すると、ビルドが継続するようになります。

test {
    ignoreFailures = true
}

sonarプラグインが動かない!

後継のsonarRunnerプラグインだとちゃんと動きました。

Gradle IDEが動かない!

Eclipseでlombokと併用すると動かないバグがあるようです。
なんかlombokとIDEという組み合わせは何かと苦しめられますね・・・。
Eclipse Grade plugin hangs when importing Gradle projects

その他に大事な事

これが頭に入ってないとタスクの動作イメージがわかないですね。この章がまさにGradle脳になるための方策を説明している気がします。

  • とにかくユーザーマニュアル、リファレンス!

DSLで簡潔な表現ができる反面、リファレンスを読まないと何ができるか分からない、という場面が非常に多かったです。
最終的にはユーザーマニュアルの章番号を覚えてしまいました。



ちょっと愚痴っぽいのも混ざってますが、良いですよGradle。

オブジェクト指向のこころ

あれから5ヶ月。やっと読み終わりました。
いやー、ちょっと間に色々やっていたもんで。

結論から言うと、オブジェクト指向に対するもやもやがかなりすっきりしました。
本当に良い本でした。
自分が感じていた違和感をすべて拭ってくれて、頭の中が整理整頓され、プログラミング中の迷いも激減しました。

  • オブジェクトは現実世界のコピーではなく責務で分ける
  • 継承より委譲
  • カプセル化とは流動的要素を隠蔽すること
  • 堅牢で柔軟なシステム、要求の変更に強いシステムを目指す


自分の性分としては、頭ごなしの暗記ではなく理屈がひとつながりになっていないと理解した気になれないのですが、この本はその道筋をちゃんと示してくれました。
なぜ、これが重要なのか。なぜそう考えるのか。どう実践していくか。


おすすめです。