Unexpected error when debugging Unicoq

[Tragicus]

Printing Unicoq's debug trace causes an "unexpected error", whenever there is something to print. It happens (at least) with coq 8.18.0 and coq-unicoq 1.6+8.18. The anomaly can be reproduced with From Unicoq Require Import Unicoq. Set Unicoq Debug. Check 0 : id nat.

[whonore]

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)

[Tragicus]

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.