チャットでも証明が書きたい

チャット上で証明が書けたら面白そうだなと思ったので、ProveEverywhere のサーバを使う hubot スクリプトを書きました。

こんなかんじ。

導入方法

(hubot 自体の導入方法については他の記事に任せます)

1. 適当なサーバに Coq 8.4 以上をインストールします。
2. prove-everywhere-server を Coq をインストールしたサーバにインストールして起動します。
3. hubot の package.json の依存ライブラリに hubot-prove-everywhere を追加します。
4. hubot の external-scripts.json に "hubot-prove-everywhere" を追加します。
5. 環境変数 HUBOT_PROVE_EVERYWHERE_URL に prove-everywhere-server が動いてるURLをセットします。
6. 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 を終了します。