概要

プログラムから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である