なつやすみのにっき
夏休みです。
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 関係だった
homebrew で MathComp を入れる
追記 2015/11/11
今だったら公式の opam リポジトリから入れたほうが簡単にマルチコアを使えて速いし安心だと思います。
opam repo add coq-released https://coq.inria.fr/opam/released # opam に Coq 関連のライブラリを追加 opam install -j4 coq.8.4.6 coq:ssreflect.1.5.0 coq:math-comp.1.5.0 # 安定版を指定してのインストール
MathComp (mathematical components) は Coq の拡張である SSReflect を使った、数学系の問題に特化したライブラリです。
で、Mac でよく使われているパッケージマネージャである homebrew には coq も ssreflect も標準であるのに、なぜか mathcomp はありません。homebrew の ssreflect formula は ssreflect-1.4 以前からあり、ssreflect は 1.5 から ssreflect と mathcomp の2つに分かれたのであってもいいはずなのですが、なぜかありません。
なので formula を作りました。
amutake/homebrew-mathcomp · GitHub
% brew tap amutake/mathcomp % brew update # 最新の ssreflect が必要なので % brew install mathcomp
これで mathcomp が入ります。mathcomp は ssreflect に依存しているので、ssreflect も入るようになっています。mathcomp のインストールは1時間くらいは普通にかかるので、気長に待ちましょう。
ところで homebrew の formula って依存パッケージのバージョンは指定できないんでしょうか…この場合だと ssreflect-1.5 が必要なので…
coqtop -emacs のプロンプト
プロンプトについて
ProofGeneral や、coqtop-vim は裏で coqtop -emacs というコマンドを実行して、そこと通信しています。
coqtop -emacs を実行すると、標準エラー出力に <prompt>Coq < 1 || 0 < </prompt> というのが出てきます。ここを見ると現在の coqtop の状態がわかります。今回の記事はこれの説明です。(もしかしたら8.4系のみ)
プロンプトの文法と意味
プロンプトの構造は
<prompt>$current_theorem < $whole_state_number |$theorem_stack1|...|$theorem_stackn| $theorem_state_number < </prompt>
となっています。それぞれについて説明します。
current_theorem
現在証明しようとしている定理の名前が入ります。 例えば、
Theorem plus_n_O : forall n : nat, n = n + O.
と入力すると、current_theorem は plus_n_O になります。
Goal forall n : nat, n = n + O.
の場合は、Unnamed_thm や Unnamed_thm0 ... となります。
証明モードに入っていないとき(トップレベルのとき)には、Coq と表示されます。
whole_state_number
その coqtop プロセスの状態番号です。一つのコマンドを行うと、1増えます。Back 1. を行うと1減って、その番号の状態になります。
theorem_stack
証明しようとしている定理のスタックです。
例えば、
Thoerem Theorem_A : ... . Proof. Theorem Theorem_B : ... . Proof.
のように、ある命題 Theorem_A の証明モードに入っているときに、命題 Theorem_B の証明モードに入ると、theorem_stack は |Theorem_B|Theorem_A| となります。Theorem_B の証明が終わると、|Theorem_A| となります。
証明モードに入っていないときにはここは空で、|| になります。
theorem_state_number
現在の証明の状態番号です。証明モードに入っていないときは0ですが、証明モードに入ると1になります。
その後、証明を進めると1ずつ増えます。証明の状態を進めるようなコマンドではないときには増えません。Qed. を行うと、0(または theorem_stack の2番めの定理の状態番号)に戻ります。
どう使うか
プロンプトを使って、コマンドの結果の出力がどのような意味を持つかを判断することができます。
例えば、
- whole_state_number も theorem_state_number も変化なし => エラー
- theorem_state_number (と whole_state_number) が変化 => 現在のサブゴールの状態
- theorem_state_number は変化せず、whole_state_number のみ変化 => その他のいろいろな情報
となります。
coqtop server を書いた
Android 開発の授業の最終課題で Android 上で動く ProofGeneral 風のアプリを作ることにしたので、JSON API で操作できる coqtop サーバを書きました。その授業の発表が終わり次第公開すると思います。
can't load .so/.DLL for: というエラー
下のようなエラーが出たとき
<command line>: can't load .so/.DLL for: /Users/amutake/work/jype/jype-doc/.cabal-sandbox/lib/x86_64-osx-ghc-7.8.2/jype-0.0.1/libHSjype-0.0.1-ghc7.8.2.dylib (dlopen(/Users/amutake/work/jype/jype-doc/. cabal-sandbox/lib/x86_64-osx-ghc-7.8.2/jype-0.0.1/libHSjype-0.0.1-ghc7.8.2.dylib, 9): Symbol not found: _jypezm0zi0zi1_DataziJypeziError_JypeCheckError_con_info Referenced from: /Users/amutake/work/jype/jype-doc/.cabal-sandbox/lib/x86_64-osx-ghc-7.8.2/jype-0.0.1/libHSjype-0.0.1-ghc7.8.2.dylib Expected in: flat namespace in /Users/amutake/work/jype/jype-doc/.cabal-sandbox/lib/x86_64-osx-ghc-7.8.2/jype-0.0.1/libHSjype-0.0.1-ghc7.8.2.dylib)
cabal ファイルの exposed-modules にモジュール名を書けば直る。 エラーがわかりにくい…
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選です。順不同。
