Ltac tac1 := fail "I failed because ...". Ltac tac2 := tac1 || fail "tac1 failed".
tac1 failed.. Is it possible to do better, and have two error messages when tac1 fails when called from tac2? the one emitted by tac1 itself, and one emitted by tac2?
Not in the current implementation of ltac afaik.
In practice, i sometimes wrote
idtac "I failed because" before the fail to print information that something failed to the user.
Sadly, in most IDEs, i think the idtac output is not presented without the user opening the associates buffer/panel by hand if the tactic failed.
yeah, I see. Thanks!
FWIW, I’d assume ltac2 has advanced features like
catch, but I guess it doesn’t help
depending on what you want,
Set Ltac Backtrace might help by adding a backtrace to ltac1’s message.
You can try replacing the Ltac1 fail by a call to a Ltac2 wrapper raising a specific exception and matching that in Ltac2-land
As long as you do not rely on the hardwired behaviour of the Ltac1 tactic failure you should be fine
(e.g. decreasing levels when crossing a match goal and the like)
can you match exceptions in Ltac2?? I understood from the manual that you can't
What the manual says is that you cannot catch panics.
But you can match on exceptions, they're defined as an extensible algebraic type in the prelude.
hmm, but then if all there is is Control.zero, that's not very useful for a tactic that uses internal backtracking
What about Control.plus?
The API for backtracking is semantically complete.
zero, plus and case are "universal" in some pedant sense
hmm, I convinced myself at some point that I couldn't reproduce the fail n behavior I wanted, but I will have to rethink about it I guess
you can use a variant of the ifthen that allows to match on your precise exception
orelse if that fits your needs better
basically I was looking for something that would reproduce the exception-like behavior of "bubble up the error up to a handler". And that doesn't really work if the inside of the tactic uses failures to backtrack. But maybe this exception-like behavior doesn't make sense in presence of backtracking?
(I'll try to come back with a more concrete example)
Backtrack is fairly different from standard exceptions.
Panics are essentially exceptions but there is currently no way to catch them
For a good reason, because the semantics becomes fuzzy when you factor in backtracking
There are various different choices and I don't know which one is correct / the best for daily use.
ok. the use-case I had in mind for catching panics was basically to catch it at the toplevel of a function, craft an error message, and rethrow
but I can imagine that it gets tricky in full generality
The main problem is how you evaluate your argument.
a.k.a. what counts as a value for a try-with block
If a fail is supposed to be fatal, you can use
fail 100 "message" to stop (100 levels) of backtracking. Of cause this can be an issue with automation, but in many cases fails are either fatal or more automation internals so that an error should be delivered later.
Last updated: Oct 01 2023 at 18:01 UTC