Keycastr と Gifzo が便利だった
utop のバグっぽいものを見つけたので、それを issue に書くために GIF のツールを使ってみた。
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
CodinGame をやってみた
面白そうなのでやってみました。
いくつか解いてみた感想
- ただのプログラミングコンテストの問題
- 標準入力から情報を受け取って、なんらかの計算をして標準出力に計算結果を出力する類の問題
- 問題のテストケースをゲームっぽくグラフィカルに表示するだけ
- 入力が何を意味しているのかや、どんな出力をすればいいのかがわかりづらい
- 普通のプロコンの問題であるような、入力と出力の例がない
- 動かしてみながら把握するしかない
- これに時間がかかってしまう
- いろんな言語が使えるのは良い
- ghc のバージョンは 7.4 だった
- なんかもっとゲームっぽいインタラクティブな何かがあるのかと思ったけど違った
追記
入力の意味やどんな結果になればいいかはゲーム画面(左上のウィンドウ)を下にスクロールしたら書いてありました……。
チャットでも証明が書きたい
チャット上で証明が書けたら面白そうだなと思ったので、ProveEverywhere のサーバを使う hubot スクリプトを書きました。
こんなかんじ。
導入方法
(hubot 自体の導入方法については他の記事に任せます)
- 適当なサーバに Coq 8.4 以上をインストールします。
- prove-everywhere-server を Coq をインストールしたサーバにインストールして起動します。
- hubot の package.json の依存ライブラリに hubot-prove-everywhere を追加します。
- hubot の external-scripts.json に "hubot-prove-everywhere" を追加します。
- 環境変数
HUBOT_PROVE_EVERYWHERE_URLに prove-everywhere-server が動いてるURLをセットします。 - 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 関係だった
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 サーバを書きました。その授業の発表が終わり次第公開すると思います。
