TC search: log hint before hint is applied#21899
TC search: log hint before hint is applied#21899Janno wants to merge 2 commits intorocq-prover:masterfrom
Conversation
This makes the output much easier to digest, especially when `Hint Extern`s produce new top-level searches.
coqbot-app
bot
added
the
needs: full CI
Janno
force-pushed
the
janno/typeclasses-debug
branch
from
d94cab7 to
893d321
Compare
| Debug: 1.1: simple apply H on foo, 1 subgoal(s) | ||
| Debug: 1.2: applying simple apply H on foo | ||
| Debug: 1.1: applied simple apply H on foo, 1 subgoal(s) |
There was a problem hiding this comment.
I'm not sure how easy it would be, but it would probably make sense to only print two lines for Hint Extern. That would reduce verbosity of traces.
Also, the numbering here looks a bit off because 1.1 comes after 1.2.
There was a problem hiding this comment.
I'm not sure how easy it would be, but it would probably make sense to only print two lines for
Hint Extern. That would reduce verbosity of traces.
That is easy to do. In that case we might want to change the output to "executing" or "running" instead of "applying". "Applying" sounds like a thing that should be printed for all hints, not just Hint Extern.
Also, the numbering here looks a bit off because
1.1comes after1.2.
I think that's just a mistake I introduced.
There was a problem hiding this comment.
I changed the output to "running", limited it to Hint Extern, and fixed the numbering issue.
Janno
force-pushed
the
janno/typeclasses-debug
branch
from
893d321 to
a8bfd81
Compare
3 participants
This adds a new line of the form
1.2.3: applying <hint> on <goal>. Without this, it is sometimes impossible to match debug output that results from running the hint to the hint, especially when aHint Externcallstypeclasses eauto.Fixes / closes #21898
make doc_gram_rsts.