デフォルトで入っている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はまだコンパイルが終わらないのでまた今度。

2014-08-27

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

定理証明定理証明支援 coq agda isabelle

定理証明支援って何？

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

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

何に役に立つの？

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

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

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

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

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

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

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

勉強すべき？

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

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

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

2013-10-31

JarファイルからManifestを読む

Java

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

Java1.7で確認済み。

2013-10-26

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

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で１件でも失敗があるとビルド失敗になってしまう

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

test {
    ignoreFailures = true
}

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

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

Gradle IDEが動かない!

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

その他に大事な事

ビルドフェーズをちゃんと理解する

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

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

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

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

2013-10-01

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

@sakamoto_desu この本おすすめですよ http://t.co/TOdRBCZF4A
— ふ''れいす (@bleis) 2013, 5月 22

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

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

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

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

おすすめです。

2013-08-21

やっぱりassertThatは良いよねという話

java

追記 2016/6/12

テスト結果のメッセージを読みやすくしたいだけなら、assertThatにreasonを書く方が楽ですね。

stackoverflow.com

    @Test
    public void test() {
        File file = new File("/tmp/hoge");
        assertThat(file.getAbsoluteFile() + " should exist", file.exists(), is(equalTo(true)));
    }

java.lang.AssertionError: /tmp/hoge should exist
Expected: is <true>
     but: was <false>

追記終わり

assertThatやっぱ便利ですねー、という話です。

assertEqualsは何のテストに失敗しているのか分かりにくかった

public class AssertEqualTests {

	@Test
	public void test() {
		final File test1 = new File("/tmp/test1.txt");
		final File test2 = new File("/tmp/test2.txt");
		final File test3 = new File("/tmp/test3.txt");
		assertEquals(true, test1.exists());
		assertEquals(true, test2.exists());
		assertEquals(true, test3.exists());
	}

}

ファイルが存在しているかどうかをテストするだけです。
で、これを実行してみると、テストが失敗しました。

java.lang.AssertionError: expected:<true> but was:<false>

これだとどのファイルで失敗したか分からないですね。
まあスタックとレースをちゃんと見れば何行目のassertEqualsで失敗しているか分かるので判定はできるのですが、あまり直感的ではありません。

Matcherを作って原因を分かりやすくしよう!

そこでassertThatとhamcrestの出番です。
もっとわかりやすいメッセージを返してくれるMatcherを作ってみました。

public class FileExist extends TypeSafeMatcher<File> {
 
    private final boolean isEexpectedResult;
    private File inspected;
 
    public FileExist(boolean exceptedResult) {
        this.isEexpectedResult = exceptedResult;
    }
 
    @Override
    public void describeTo(Description description) {
        description.appendText(inspected.getAbsolutePath());
        if (isEexpectedResult) {
            description.appendText(" exist");
        } else {
            description.appendText(" does not exist");
        }
 
    }
 
    @Override
    protected void describeMismatchSafely(File item, Description mismatchDescription) {
        mismatchDescription.appendText(inspected.getName());
        if (isEexpectedResult) {
            mismatchDescription.appendText(" does not exist.");
        } else {
            mismatchDescription.appendText(" exist.");
        }
 
    }
 
    @Override
    protected boolean matchesSafely(File item) {
        this.inspected = item;
        return item.exists() == isEexpectedResult;
    }
 
    @Factory
    public static <T> Matcher<File> exist() {
        return new FileExist(true);
    }
 
    @Factory
    public static <T> Matcher<File> NotExist() {
        return new FileExist(false);
    }
 
}

TypeSafeMatcherを継承して独自Matcherを作っています。
ファイルを受け取って期待通り存在しているか、もしくは存在していないかをテストできます。
そしてdescribeToで成功時のメッセージを、describeMismatchSafelyで失敗時のメッセージを作成しています。

テストは以下のようになります。

public class AssertThatTests {

	@Test
	public void test() {
		final File test1 = new File("/tmp/test1.txt");
		final File test2 = new File("/tmp/test2.txt");
		final File test3 = new File("/tmp/test3.txt");
		assertThat(test1,exist());
		assertThat(test2,exist());
		assertThat(test3,exist());
	}

}

そして実行結果。

java.lang.AssertionError: 
Expected: /tmp/test2.txt exist
     but: test2.txt does not exist.

test2.txtが存在していないというのが一目でわかりますねー。素敵です。
Matcherを簡単に作れるというのは、結果の分かりやすくする事にも役立つんですね。

ちょっとはまったこと。

Matcherを作るとき、どうしてもdescribeMismatchSafelyが見つからず@Overrideがエラーを吐いてしまいました。
原因は我らがstackoverflowで見つかりました。

junitライブラリ内部の古いhamcrestを参照してるんじゃない？今はhamcrestは別ライブラリだよ
Junitを4.10以上にして、junit.jarとhamcrest-core.jarをビルドパスに加えてみ
hamcrest-core.jarはjunit.jarより上位にしてね

600000007

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

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

LTで言えなかった事

LTをやってみた感想

Macでssreflect

CoqIDE or ProofGeneral

Emacs