概要
プログラムからemacsモードを用いてCoqを操作するための参考文書です。
基本はこちらのサイトに詳しい: http://amutake.hatenablog.com/entry/2014/07/07/020814
ざっくり言うと
-
coqtop -emacsで起動するとProofGeneralなどから使用するためのemacsモードに入る - EmacsモードはプログラムとCoqがやり取りするのに (やや) 向いている
- コマンドの実行結果は標準出力に、プロンプトは標準エラーに出る。Warningなどは標準エラーに出る
- 実行結果は (ほぼ確実に) 改行で終わるが、プロンプトには改行はつかない
- (ほぼ確実に) 標準エラーにプロンプトが出た時点で、標準出力には実行結果がすべて出力されている
となる。「(ほぼ確実に)」というのは、今のところ著者はこれに違反する例は見つけていないが、仕様上そうなっているかは確信できない、という意味。起動時もほぼ同様で、起動後、
- 標準出力にCoqのバージョンが (改行付きで) 出る
- -l オプションで指定したファイルを読み込み、標準出力と標準エラーにメッセージが出る
- すべての標準出力などが出たら、プロンプトが標準エラーに出る
というプロセスを辿る。実際には -l <ファイル名> を複数回指定することにより、起動時に複数のファイルをロードすることができる。この時にプロンプトが出力されるのは複数回または1回のどちらかであるか、については未確認である。
プログラムするなら
よって、プログラムを書くなら大体このようになる
起動時
- Coqのプロセスを起動する
- (必要があれば) 標準出力から1行読み込んでバージョンをコンソールに出力するなりする
- 以下をプロセスがブロックしないように適宜交互に行う
- 標準出力から行単位で読み込む
- 標準エラーから文字単位で読み込む
- 標準出力から読める文字 (行?) がなくて、標準エラーの末尾がプロンプトなら、Coqはreadyである
コマンド実行時
複数のコマンドを投げるときは、以下のプロセスをコマンド毎に繰り返すのが無難
- Coqのプロセスの標準入力にコマンド+改行を投げる
- 以下をプロセスがブロックしないように適宜交互に行う
- 標準出力から行単位で読み込む
- 標準エラーから文字単位で読み込む
- 標準出力から読める文字 (行?) がなくて、標準エラーの末尾がプロンプトなら、コマンドの結果はすべて出力され、Coqはreadyである