ocamldebugを使うのを諦めた

Coqのソースコードをocamldebugで追えるようにして早何日か。

結局ocamldebugを使うのは（少なくとも現時点では）諦めることにした。

理由は次の通り。

1. Coqが使っている構文解析器がそもそもocamlcでコンパイルするものじゃなかった*1。
2. 多相がものすごく邪魔だった。途中から<poly>と見ただけでひっくり返したくなった。
3. ブレイクポイントが結構荒っぽかった。
4. ソースコードがない部分があった*2。

これだけあれば諦めもつくし、しかも２〜３時間程度でひとまず構文の追加に成功したので、いろんな意味で遠回りしすぎたと言える。

*1：どうもcamlp4をそのまま使っているようだ。

*2：字句解析のコードがテンポラリフォルダに作られて、すぐ消されていたようだ。