Stream: Coq users

Topic: ltac: combined fail error messages


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Armaël Guéneau (Nov 26 2020 at 21:48):

yeah, I see. Thanks!

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Nov 27 2020 at 02:09):

*to tac1’s message

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Nov 27 2020 at 10:05):

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

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Nov 27 2020 at 10:22):

What the manual says is that you cannot catch panics.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Nov 27 2020 at 10:23):

What about Control.plus?

view this post on Zulip Pierre-Marie Pédrot (Nov 27 2020 at 10:24):

The API for backtracking is semantically complete.

view this post on Zulip Pierre-Marie Pédrot (Nov 27 2020 at 10:24):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Nov 27 2020 at 10:26):

ifcatch sorry

view this post on Zulip Pierre-Marie Pédrot (Nov 27 2020 at 10:26):

or orelse if that fits your needs better

view this post on Zulip 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?

view this post on Zulip Armaël Guéneau (Nov 27 2020 at 10:30):

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

view this post on Zulip Pierre-Marie Pédrot (Nov 27 2020 at 10:30):

Backtrack is fairly different from standard exceptions.

view this post on Zulip Armaël Guéneau (Nov 27 2020 at 10:30):

right

view this post on Zulip Pierre-Marie Pédrot (Nov 27 2020 at 10:31):

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

view this post on Zulip Pierre-Marie Pédrot (Nov 27 2020 at 10:31):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Armaël Guéneau (Nov 27 2020 at 10:33):

but I can imagine that it gets tricky in full generality

view this post on Zulip Pierre-Marie Pédrot (Nov 27 2020 at 10:34):

The main problem is how you evaluate your argument.

view this post on Zulip Pierre-Marie Pédrot (Nov 27 2020 at 10:34):

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

view this post on Zulip 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: Jan 27 2023 at 01:03 UTC