Stream: Elpi users & devs

Topic: Catch elpi tactics failures with try

Chantal Keller (Sep 13 2023 at 16:16):

Hi
I would like to have the Ltac try catch failures caused by elpi tactics. Here is an example:

From elpi Require Import elpi.

Elpi Tactic foo.

Elpi Accumulate lp:{{
  solve _InitialGoal _NewGoals :-
    std.assert! false "bar".
}}.
Elpi Typecheck.

Goal False. try elpi foo.

and similarly if the tactic fails with the error The elpi tactic ... failed without giving a specific error message.
Is it possible?
Thanks!

Enrico Tassi (Sep 13 2023 at 21:30):

Yes it is possible but badly documented, sorry for that.

You can use the @ltacfail! option to the std.assert family of API as per the changelog entry https://github.com/LPCIC/coq-elpi/blob/master/Changelog.md#1100---21-05-2021 , or call coq.ltac.fail directly if you need to abort with a catchable exception.

See this example in algebra-tactics: https://github.com/search?q=repo%3Amath-comp%2Falgebra-tactics%20%40ltacfail!&type=code

Chantal Keller (Sep 14 2023 at 05:51):

Thank you!

Chantal Keller (Sep 14 2023 at 05:51):

I gues in the case of The elpi tactic ... failed without giving a specific error message. it won't work, I have to manually throw an error in elpi?

Enrico Tassi (Sep 28 2023 at 11:38):

Yes, see coq.ltac.fail API.

Last updated: Oct 13 2024 at 01:02 UTC