Hello. Is there another way to find where and why a predicate failed than
coq.saydebug which is not very pleasant either ?
You can use
(it will log the input and output of a clause)
A trace browser is planned, and engineering manpower allocated... then there was the pandemic and it stalled.
The best you can get is by
Elpi Trace "predicate" so that only goals about "predicate" are displayed. It's actually a regex following OCaml's conventions.
If you have ideas on what exactly a trace browser should let you do/filter/jump-to, I'm all ears. I've some ideas, but my POV is probably biased.
Last updated: Jun 06 2023 at 22:01 UTC