Stream: Coq users

Topic: ltac: combined fail error messages

Armaël Guéneau (Nov 26 2020 at 19:09):

    Ltac tac1 :=
      fail "I failed because ...".
    Ltac tac2 :=
      tac1 || fail "tac1 failed".

This prints 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?

Fabian Kunze (Nov 26 2020 at 20:54):

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.

Armaël Guéneau (Nov 26 2020 at 21:48):

yeah, I see. Thanks!

Paolo Giarrusso (Nov 27 2020 at 02:08):

FWIW, I’d assume ltac2 has advanced features like catch, but I guess it doesn’t help

Paolo Giarrusso (Nov 27 2020 at 02:09):

depending on what you want, Set Ltac Backtrace might help by adding a backtrace to ltac1’s message.

Paolo Giarrusso (Nov 27 2020 at 02:09):

*to tac1’s message

Pierre-Marie Pédrot (Nov 27 2020 at 10:04):

You can try replacing the Ltac1 fail by a call to a Ltac2 wrapper raising a specific exception and matching that in Ltac2-land

Pierre-Marie Pédrot (Nov 27 2020 at 10:05):

As long as you do not rely on the hardwired behaviour of the Ltac1 tactic failure you should be fine

Pierre-Marie Pédrot (Nov 27 2020 at 10:05):

(e.g. decreasing levels when crossing a match goal and the like)

Armaël Guéneau (Nov 27 2020 at 10:22):

can you match exceptions in Ltac2?? I understood from the manual that you can't

Pierre-Marie Pédrot (Nov 27 2020 at 10:22):

What the manual says is that you cannot catch panics.

Pierre-Marie Pédrot (Nov 27 2020 at 10:23):

But you can match on exceptions, they're defined as an extensible algebraic type in the prelude.

Armaël Guéneau (Nov 27 2020 at 10:23):

hmm, but then if all there is is Control.zero, that's not very useful for a tactic that uses internal backtracking

Pierre-Marie Pédrot (Nov 27 2020 at 10:23):

What about Control.plus?

Pierre-Marie Pédrot (Nov 27 2020 at 10:24):

The API for backtracking is semantically complete.

Pierre-Marie Pédrot (Nov 27 2020 at 10:24):

zero, plus and case are "universal" in some pedant sense

Armaël Guéneau (Nov 27 2020 at 10:25):

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

Pierre-Marie Pédrot (Nov 27 2020 at 10:25):

you can use a variant of the ifthen that allows to match on your precise exception

Pierre-Marie Pédrot (Nov 27 2020 at 10:26):

ifcatch sorry

Pierre-Marie Pédrot (Nov 27 2020 at 10:26):

or orelse if that fits your needs better

Armaël Guéneau (Nov 27 2020 at 10:29):

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?

Armaël Guéneau (Nov 27 2020 at 10:30):

(I'll try to come back with a more concrete example)

Pierre-Marie Pédrot (Nov 27 2020 at 10:30):

Backtrack is fairly different from standard exceptions.

Armaël Guéneau (Nov 27 2020 at 10:30):

right

Pierre-Marie Pédrot (Nov 27 2020 at 10:31):

Panics are essentially exceptions but there is currently no way to catch them

Pierre-Marie Pédrot (Nov 27 2020 at 10:31):

For a good reason, because the semantics becomes fuzzy when you factor in backtracking

Pierre-Marie Pédrot (Nov 27 2020 at 10:32):

There are various different choices and I don't know which one is correct / the best for daily use.

Armaël Guéneau (Nov 27 2020 at 10:33):

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

Armaël Guéneau (Nov 27 2020 at 10:33):

but I can imagine that it gets tricky in full generality

Pierre-Marie Pédrot (Nov 27 2020 at 10:34):

The main problem is how you evaluate your argument.

Pierre-Marie Pédrot (Nov 27 2020 at 10:34):

a.k.a. what counts as a value for a try-with block

Michael Soegtrop (Nov 28 2020 at 10:41):

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