Unexpected error when debugging Unicoq about coqtail HOT 2 CLOSED

The issue is Check 0 : id nat is causing a warning to be printed to stderr. Coqtail tries to distinguish between warnings and errors, but the only way to do that is with heuristics about what shape the warning has, and Unicoq isn't following the expected pattern (there's no [warning type] at the end), so Coqtail treats it like an error.

I think what I'll do is to add an option that lets you try to progress even if there's an error on stderr, and maybe also adjust/relax the warning regex.

The warning from Unicoq is:

Warning: no LaTex file set with [Set Unicoq LaTex File 'file']. No LaTex output will be generated.
?A =<= Set (Meta-Inst) OK
_Type =<= Type (Reduce-Same)

from coqtail.

I see, thanks. This is weird, because Unicoq only uses Printf.printf and never mentions stderr. However, I changed all the printf by coq's feedback functions and the issue disappeared.
I close this since the issue is resolved, though the improvements you mentioned would be great.

from coqtail.