You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
The text was updated successfully, but these errors were encountered:
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)
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.
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.
The text was updated successfully, but these errors were encountered: