Combination of ProofGeneral and Org-mode (experimental)
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
doc
examples
.gitignore
README.org
note.org
ox-coq.el
pg-org.el

README.org

PG-Org mode: interactive proof and documentation

概要

Org-mode でテキストを書きながら Proof General みたいに Coq コード書いて評価! をしたいなぁと思った結果生まれた Org-mode を拡張したような感じのそれです。

特に、証明中のゴールとかをぽんぽんと挿入したいなぁと思っていたので、そんな機能も入っています。

あまり重いコードには使わない方が幸せだと思います(私は試していません)。

ちょっと変なことするとすぐにめんどくさくなるので、何かあったら C-c C-x するのがいいと思うよ。

使い方

1/16(fri) に Org mode 用の Coq スクリプトエクスポータの ox-coq.el を使うようになりました。 作ったの僕なんですけどね、しかもかなりのプロトタイプ。

  1. ProofGeneral を使えるようにしておく。
  2. Org-mode も使えるようにしておく。
  3. ox-coq.el をパスの通る場所に置いて (load "ox-coq.el") しておく。
  4. pg-org.el をパスの通る場所に置いて (load "pg-org.el") しておく。
  5. auto-mode-alist とか使って pg-org-mode と何かを関連付けておくとよい。

設定例

(load "ox-coq")
(load "pg-org")
(add-to-list 'auto-mode-alist '("\\.org$" . pg-org-mode))

キーバインド

org-mode の派生モードなので、 org-mode で使える機能は(多分)使えます。 肝はやっぱエクスポートかなー。

pg-org-mode には現時点で七つの機能があり、それぞれにキーバインドが設定してあります。

各機能は、評価系、挿入系、その他の三つに分類されています。

評価系

ProofGeneral と同じ雰囲気で。

C-c C-<return>
現在のカーソルがあるソースブロックまでを評価。
C-c C-n
これまでに評価してきたソースブロックたちの、次の一つを評価。
C-c C-u
ソースブロックの評価を一つ戻す(実態は、一つ前のソースブロックまでの評価)。

挿入系

現在、挿入されるものは全て EXAMPLE ブロックとして挿入(#+BEGIN_EXAMPLE ... #+END_EXAMPLE で囲われる)されます。

C-c C-;
直前の評価結果を挿入。 ComputeCheck のあとに使うと便利。
C-c C-i g
現在証明中のゴールを一つ挿入。複数のサブゴールがあるときは番号を聞かれます。
C-c C-i c
入力されたコマンドを評価し、その結果を挿入。ピリオドは忘れずに。

その他

C-c C-x C-e
問答無用で評価中止。気を付けよう。

今後

まだまだ機能が足りていないので、やりたいことを全て列挙するのは難しいのですが、 代表的なものを書いてみます。

評価位置の計算方法

今の評価位置の決定方法は非常に雑で、 ソースブロック外のテキストが大幅に変更されたりすると思っていたところとは違うポイントまで 評価されることがあります。

ソースブロックの位置を適切に監視できる方法などが要りそうです。

バッファの表示

ProofGeneral のようにハイライト付けるか、 評価済みのソースブロックに印を付けるか、 いずれにせよどこまで評価したかが見てわかるようにしたい。

ブロックの区別

今は全部 EXAMPLE ブロックでの挿入なのですが、 これだと挿入後に区別できなくなってしまいます。

ゴールなら #+BEGIN_GOAL ... #+END_GOAL で括るとかしておきたいですね。

すぐにやれそうだなこれ。

ユニコード文字への変換表示

ProofGeneral の unicode-tokens-mode でショートカットを disable にした状態と同じことがしたいなぁと思っています。

alpha って入力したら 𝞪 って表示されるようなアレです。

coq-unicode-tokens.el を参考にすればよさそう。

org-edit-special の挙動

Org-mode の機能として、ブロック内で =C-c ‘= すると(指定されていれば)適切なメジャーモードで そのブロック内を編集できるという素敵なものがあります。

pg-org-mode 中でも当然それができるのですが、 これを実行すると現在のフレームが vorg ファイルのバッファとブロックだけを抽出したバッファの二つのみに なってしまって、ゴールの確認とかがしづらいです。

対話的証明とはなんだったのかという思いが頭を過るので、バッファの分割法などを調整するつもりです。