I’m trying to fix a bug in my Vim plugin that communicates with Coq using the XML interface (https://github.com/whonore/Coqtail/issues/56#issuecomment-518334010) where certain error messages are duplicated. It seems that the messages sometimes appear both in a <value val="fail"> tag and a <feedback> tag, but I haven’t figured out yet in what cases I’m supposed to ignore one or the other. I tried looking through the code in ide/idetop.ml and some of the related files since CoqIDE and coqtop don’t seem to have this issue, but I’m not very familiar with OCaml so I couldn’t tell how they handle it. Any advice or pointers to the relevant pieces of code would be much appreciated.
Different Coq versions are buggy in different ways; unfortunately if you use all the advanced features of the XML protocol there is no 100% reliable way of getting errors reported.
If you use the XML protocol mostly on a synchronous fashion, then the standard workaround is just to listen to fail values and ignore feedbacks with the Error tag set.
More information: https://github.com/coq/coq/issues/5479
Thanks, I’ll try that.