Raising the failure level of a coq tactic

Question

When implementing a complex tactic in Ltac, there are some Ltac commands or tactic invocation that I expect to fail and where that is expected (e.g. to terminate a repeat, or to cause backtracking). These failures are usually raised at failure level 0.

Failures raised at higher level “escape” the surrounding try or repeat block, and are useful to signal unexpected failures.

What I am missing is a way to run a tactic tac and treat its failure, even at level 0, to be at a higher level, while retaining the message of the failure. This would let me make sure that repeat does not terminate due to a Ltac programming error on my side.

Can I implement such a failure-raising-level higher-order tactic in Ltac?

Extrovert

Answer 1

You can write a tactic to achieve that in Ocaml. I put that on GitHub here.

For example the following should raise an error instead of silently succeeding:

repeat (match goal with 
          | [ |- _ ] => 
            raise_error_level (assert (3 = 3) by idtac)
        end).

Disagree

Answer 2

I do not know if it is possible to get exactly what you want, but I sometimes use the following idiom:

tactic_expression_that_may_fail_with_level_0
|| fail 1000 "There was some problem here"

If the first tactic fails with level 0, the || will try to run the second one, which will fail with a very high level and report it to you.

It would help if you could provide a concrete use case to see if some other technique would be better suited.

Ewell

Your work around does exactly what I want (and I used it so far), with the exception that I lose the actual information on the level-0 failure, which, for a few tactics, can actually be quite useful. – Extrovert