Coq-8.5の実装内にプリンタを加える（メモ）

Coq-8.5pl1でタクティクスを実行する際に呼ばれている関数を判別する為にプリンタを実装内に加えた際の備忘録。

• Coq-8.5pl1のコンパイル時にプリント出力が作動しない様、flagsでデバッグ用フラグを定義。falseに初期化しておく。

  coq-8.5pl1/lib/flags.mli

    val my_debug : bool ref
  

  coq-8.5pl1/lib/flags.ml

    let my_debug = ref false
  

• 必要な場所に以下の様なフラグでの条件付きプリンタを設置。

  if !Flags.my_debug then
  begin
  …
  Pp.msg_debug (Pp.str “here we write a message…“);
  …
  end;

  型によってプリンタが用意されているものがあり、c: constr を表示する場合は

  Pp.msg_debug (Termops.print_constr c);

  env: envを表示する場合は

  Pp.msg_debug (Termops.print_env env);

  sigma: evar_mapを表示する場合は

  Pp.msg_debug (Evd.pr_evar_map None sigma);

  等。

• Coqをコンパイル、そしてインストール。例：

  make -j3
  sudo make install

• 以下のプラグインもどきを任意のディレクトリ（ここではmy_plugin）に作成しデバッグ用のフラグを立てる。

  my_plugin/dbgprt_plugin.ml4

    DECLARE PLUGIN "dbgprt_plugin"
    Flags.my_debug := true;; 
  

• CoqのMakefileをmy_plugin内に作成し実行

coq_makefile dbgprt_plugin.ml4 -o Makefile
make

• my_plugin内でcoqtop又はProofGeneralを実行。書き出しに以下の宣言を加える。　

  Declare ML Module "dbgprt_plugin".

• ProofGeneralを使用する場合、emacs設定ファイルのcoq-load-pathに上記のmy_pluginを加えておく。

以上