cabal-install の bootstrap.sh で module ‘foobar-0.0.0:Main’ is defined in multiple files ...

cabal-install の bootstrap.sh で module ‘stm-2.4.3:Main’ is defined in multiple files: ... みたいなエラーが出てコケたときは、

% cd stm-2.4.3
% ./Setup install
% cd ../
% ./bootstrap.sh

とやればよい。仕組みは不明。

$GOPATH

golang の GOPATH について。

昨日まで GOPATH で指定したディレクトリは、Haskell の .cabal ディレクトリみたいにパッケージがインストールされるだけの場所だと思ってたけど、自分でコードを書くときもこの中で作業をするということを知った。

研究室の先輩のリポジトリとか見ると、

import (
    "github.com/username/repo/package1"
    "github.com/username/repo/package2"
)

こんなふうに書いてあって、「必ず github とかに上げないといけないのだろうか…」とか思ってたけど、GOPATH の中で直接作業をすることで github に上げなくても良くなってる。

いままでそこら辺に転がっている個人のブログしか見てなかったけど、ちゃんと公式のドキュメントに書いてた。 http://golang.org/doc/code.html

更新を楽しみにしているWeb漫画10

個人的に更新を楽しみにしているWeb漫画10選です。順不同。

• パペラキュウ
• All You Need Is Kill
• 市場クロガネは稼ぎたい
• はるこ少女期
• 徒然チルドレン
• 働かないふたり
• 俺とヒーローと魔法少女
• T.Yめもり～ず
• アクアの魔法
• 裏ジャック

Why3 で遊んでみた

Why3 で遊んでみたのでメモ．インストールで手間取った．環境は Mac OS X 10.9.1 です．

Why3 のインストール

※この方法は Mac OS X かつ Homebrew 専用です．Linux や MacPorts でのインストールはわかりません．

ソースからは面倒なので，OCaml のパッケージマネージャである opam でいれます．(追記: https://github.com/mht208/homebrew-formal に Why3 の formulae があったのでそっちのほうが簡単かもしれない(試してない))

まず依存ライブラリなどをインストール．

• XQuartz をインストール
  • インストール後は再ログインが必要かもしれない
• brew install gmp
• brew install gtksourceview
  • XQuartz が必要

次に，https://github.com/OCamlPro/ocaml-top/issues/42#issuecomment-22091964 に書いてあるように，下のスクリプトを .zshrc か何かに書きこんで source .zshrc をします．これをしないと conf-gtksourceview をインストールするときにコケます．

export PKG_CONFIG_PATH=$PKG_CONFIG_PATH:/usr/X11/lib/pkgconfig/
for i in `ls /usr/local/opt/`;
do
    if [ -d "/usr/local/opt/$i/lib/pkgconfig" ];
    then export PKG_CONFIG_PATH=$PKG_CONFIG_PATH:"/usr/local/opt/$i/lib/pkgconfig";
    fi;
done

最後に opam install why3 でインストールできます．たぶん．

% why3 --version
Why3 platform, version 0.82 (build date: Fri Jan 17 00:48:01 JST 2014)

Why3IDE で遊んでみる

Why3 には IDE が付属しているので，それで遊んでみます．

IDE を起動させる前に，まずは Prover を探させます．

% why3config --detect-provers
Found prover Alt-Ergo version 0.95.2, Ok.
Warning: prover Coq version 8.4pl3 is not known to be supported.
1 provers detected and 1 provers detected with unsupported version
== Found /Users/amutake/.opam/4.01.0/lib/why3/lib/why3/plugins/dimacs.cmxs ==
== Found /Users/amutake/.opam/4.01.0/lib/why3/lib/why3/plugins/genequlin.cmxs ==
== Found /Users/amutake/.opam/4.01.0/lib/why3/lib/why3/plugins/hypothesis_selection.cmxs ==
== Found /Users/amutake/.opam/4.01.0/lib/why3/lib/why3/plugins/tptp.cmxs ==
Save config to /Users/amutake/.why3.conf

なんか Coq 8.4pl3 で Warning でてるけど気にしない．

why3ide コマンドで起動．

% why3ide .
[Info] Init the GTK interface... done.
[Info] reading icons... done.
[Info] Creating tree model... done
[Info] found directory '.' for the project
[Info] Opening session...

[Info] Opening session: update done

[Info] Opening session: done

これで X11 が立ち上がって IDE が起動するはずです．起動しない場合は XQuartz.app を立ち上げた状態で実行してみたり，マシンを再起動してみたりすると直るかもしれません．

Hello Proofs!

さて，無事起動できたので，マニュアルの 1.1 Hello Proofs をやってみます．

一旦 IDE を閉じて，以下の内容の hello_proof.why というファイルを作ってください．

theory HelloProof "My very first Why3 theory"

  goal G1 : true

  goal G2 : (true -> false) /\ (true \/ false)

  use import int.Int

  goal G3 : forall x : int. x * x >= 0

end

そしてターミナルで why3ide hello_proof.why とやると，hello_proof.why を読み込んだ IDE が起動します．

こんなかんじになるはずです．

G1 を選択して，左の Alt-Ergo ボタンを押してみましょう．

緑のチェックマークがつきました．G1 : true という命題が証明された，ということです．

HelloProof を選択して左の Alt-Ergo ボタンを押してみると，こうなります．

G2 : (true -> false) /\ (true \/ false) が残りました． 次はこの G2 をCoqを使って証明し(ようとし)てみます．

G2 を選択して，Coq ボタンを押してください．できた行を選択すると "Please Edit" と書いてあるので，左の Edit ボタンを押します．

hello_proof.why があるディレクトリに hello_proof というディレクトリができ，その中に hello_proof_HelloProof_G2_1.v というCoqのソースファイルができます．このファイルの内容は以下のようになっています．

明らかにこれは証明できません! 命題を編集して証明できるものにしましょう． 現在の Why3IDE は why ファイルを直接編集することはできないので，適当なテキストエディタで G2 を以下のように編集します．

goal G2 : (false -> false) /\ (true \/ false)

編集したら，IDE に戻ってリロード(Ctrl-r)します．obsolete になります．

G2 を選択して Alt-Ergo，Coq ボタンを押すと，もう一度 try させることができます．代わりに左上のラジオボタンを All goals にして Replay ボタンを押しても同じことができます．

Alt-Ergo で証明できてしまいましたが，せっかくなので Coq でも証明してみたいと思います．

hello_proof/hello_proof_HelloProof_G2_1.v を開くと，Theorem G2 : False. だったのがTheorem G2 : True. になっています．これは auto タクティクで証明できそうです．

保存したら IDE に戻り，G2 の Coq の行を選択して，左の Coq ボタンを押します．

緑のチェックマークがつきました!

まとめ

• Why3 をインストールしてみたよ．Why3 のインストールはすこし面倒だった．
• Why3IDE を使って簡単な命題を証明してみたよ．

Idris 0.9.10

idris-0.9.10 がリリースされたのでちょっと触ってみた。http://www.idris-lang.org/idris-0-9-10-released/

証明付き型クラス

以前の idris では下のツイートのようなことはできなかったのですが、できるようになっていました。

型クラスを実装するときに、性質を満たすことを証明しないと通らないみたいなことってできないのか…

— あむ (@amutake_s) August 31, 2013

例えば、

class MySemigroup a where
  (<+>) : a -> a -> a
  mySemigroupOplsAssociative : (x, y, z : a) -> x <+> (y <+> z) = (x <+> y) <+> z

のように、型クラスの実装に性質の証明を要請することができるようになりました。0.9.9以前でこのクラス定義のようなことをしようとすると、 <+> が見つからないとかで型チェックが通らなかった(はず。よく覚えてない)。

でも Prelude.Algebra モジュール が未だに性質の部分を Vierified なんちゃら型クラスとして分離させているのはなぜだろう。

他

他の変更点としては、とうとう OS X 向けのバイナリが出たりとか、この前書いたようにサーバ・クライアントで動くようになったりとか、llvm, gmp, ffi がデフォルトでは無効になったりとか。あまりちゃんと調べていないけどこんなところかなあ。

idris-mode for Vim/Emacs

最近巷で話題の Idris (依存型を持つ純粋関数型言語)ですが、この Idris にも vim と emacs のプラグインがあります。

idris-vim

vim の idris-mode です。Idris のメイン開発者である Edwin Brady さんも開発に加わっています。

• リポジトリ
• Edwin Brady さんのブログポスト

※ 2013-11-1現在では Hackage にある idris-0.9.9.3 では動きません。 idris-0.9.10 を待つか、 idris の HEAD で試してください。

インストール

neobundle を使っている人は NeoBundle 'idris-hackers/idris-vim' で入ります。Vundle でも同じかんじで入ると思います。

確認していませんが、もしかすると syntastic と vimshell がないと正常に動かないかもしれません。

使い方

<leader> は Vim の leader-key というやつです。デフォルトでは \ です。

• <leader>t
  • カーソル下にあるシンボルの型を表示
• <leader>e
  • 入力された式を評価するプロンプトが表示される
• <leader>r
  • カレントバッファの型チェックを行う
• <leader>c
  • カーソルが場合分けを行う変数の上にあるときは、パターンが網羅されるように場合分けが展開される
• <leader>w
  • f x y z = ?rhs の形をしているとき、with-パターンを挿入する
• <leader>d
  • カーソルがトップレベルにある関数の型シグネチャの上(: の右側)にあるときは、関数の定義のフォーマットを挿入する

というキーバインドになっています。

以下のようにすると、(たぶん) vim が開くので、これで上のコマンドが使えるようになります。

% idris test.idr    
     ____    __     _                                                                    
    /  _/___/ /____(_)____        
    / // __  / ___/ / ___/     Version 0.9.9.3   
  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/         
 /___/\__,_/_/  /_/____/       Type :? for help                              
                                                                                         
Type checking test.idr
*test> :e

なぜ一旦 idris の REPL を起動しないといけないかというと、 REPL を起動すると repl-server というのがポート4294で起動して、そこに向けてコマンド(idris --client :l <idris-file> など)を投げるという実装になっているからです。

正直 REPL を経由するのは面倒なのでしないでもよくなってほしいです。

[追記] https://github.com/amutake/idris-vim いちいち REPL を起動しなくてよくしてみました。 vimproc が必要です。vim 歴一週間くらいなのでこれでいいのかよくわかっていません。

vim-mode

emacs の idris-mode です。

• リポジトリ

インストール

el-get を使っている人は、公式のレシピの中に既に入っているので、(el-get 'sync 'idris-mode) でインストールできます。 それ以外の人は、ロードパスを通して(require 'idris-mode) をすると、*.idr ファイルを開いた時に自動的に idris-mode になります。

使い方

C-c C-l とタイプすると、そのファイルがロードされた Idris の REPL が開きます。ロードできなかったときはエラーの場所をハイライトしてくれます。

......のはずですが、CUI 版の emacs だと、エラーの場合はいいのですが REPL を開いてコマンドを打ったとき、応答がなくなってしまいます。

また、GUI 版の emacs だと、REPL からの応答はあるのですが、文字化けしているようになってしまいます(おそらく Idris の REPL は色を付けて表示する機能が付いているからだと思います)。

動いたらまた追記したいと思います。

まとめ

• idris も Vim/Emacs のモードがあるよ。
• idris-vim のほうが多機能。
• ちゃんと動かすのは難しいかもしれない。シンタックスハイライトとインデントをしてくれるだけでもいいなら。
• この idris-hackers というグループこわい。

OS X Mavericks にしたら gcc を使う Haskell パッケージがビルドできなくなった件

参照: http://cp.reddit.com/r/haskell/comments/1ozukp/anyone_running_ghc_763_on_osx_mavericks/

Xcode 5 が clang を使っていて gcc4.2 を提供しなくなったせいらしい。

clang に対応している GHC7.8 が出るまで待つか GHC HEAD を使えばいいらしいけど、以下のようにしてもいい。

% brew install apple-gcc42
...
% which gcc-4.2
/usr/local/bin/gcc-4.2
% ghc-pkd list | head -1
/usr/local/Cellar/ghc/7.6.3/lib/ghc-7.6.3/package.conf.d 
% $EDITOR /usr/local/Cellar/ghc/7.6.3/lib/ghc-7.6.3/settings
  ...
  ("C compiler command", "/usr/local/bin/gcc-4.2") # ここを gcc-4.2 に変える
  ...

以上で一応動くようになった。

Xcode 5 と ghc-7.6.3 の相性がアレなことは周りで散々言われていたことのようだったので情弱でした。