ocamldebugを使うのを諦めた

Coqのソースコードをocamldebugで追えるようにして早何日か。
結局ocamldebugを使うのは（少なくとも現時点では）諦めることにした。
理由は次の通り。

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

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

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

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