Luko van der Maas (Sep 28 2023 at 11:17): Luko van der Maas (Sep 28 2023 at 11:17):Hi me again,
Is there a way to see why an elaboration failed? I have now multiple times had to debug a failed elaboration and some way to see why it failed would make debugging them a lot easier. The tracer is already very useful to see where it actually goes wrong, but finding out why still takes a long time.
Enrico Tassi (Sep 28 2023 at 11:26):what do you mean exactly by "elaboration"? A call to coq.elaborate-*?
Luko van der Maas (Sep 28 2023 at 11:30):Yes, so I call refine, which internally calls coq.elaborate-skeleton, which fails. And I would like to know why it fails.
Enrico Tassi (Sep 28 2023 at 11:36):Oh, I see. The easiest for now is that you edit this line: https://github.com/LPCIC/coq-elpi/blob/master/elpi/elpi-ltac.elpi#L14
The idiom is
std.assert-ok! (coq.elaborate-skeleton T TY TR) "refine error:",
The ok argument here is "imposed", but the API is likely to return error Message.
The assert-ok! API prints the Message and aborts the execution.
If you want a non-fatal failure, write something
coq.elaborate-skeleton T TY TR D,
if (D = error Msg) (coq.say Msg, fail) true,
instead.
Luko van der Maas (Sep 28 2023 at 11:38):That is perfect, thank you very much. I really like the language so far, and your support helps a lot :)
Notification Bot (Sep 28 2023 at 11:38):Luko van der Maas has marked this topic as resolved.
Enrico Tassi (Sep 28 2023 at 11:38): Enrico Tassi (Sep 28 2023 at 11:39):In case you want to turn the fatal error into an Ltac error, which could be printed by Ltac (or catched).
Notification Bot (Sep 28 2023 at 11:39):Enrico Tassi has marked this topic as unresolved.
Enrico Tassi (Sep 28 2023 at 11:41):I'm also fine adding a variant of refine which returns the diagnostic, if it is what you need to write a user friendly tactic.
Or you can just submit a PR with it.
Notification Bot (Sep 28 2023 at 11:41):Enrico Tassi has marked this topic as resolved.
Luko van der Maas (Sep 28 2023 at 11:45):I'll make the PR if I need it besides debug purposes
Last updated: Oct 13 2024 at 01:02 UTC