Consistent error messages for internal IPM failures
There are a couple of places where an IPM tactic could theoretically fail in strange cases. The treatment of such cases is not consistent.
When defining a tactic in ltac_tactics
, sideconditions of a lemma from coq_tactics
that should be always be solvable by a single tactic tac
:
- are sometimes just handled with
tac
- are sometimes handled as
tac || fail "some error message which might make clear that this should not happen"
Some examples are in iInduction, iLöb and iPoseProofCoreLem.
As discussed here, it would be nice if such cases were handled consistently.
A possible fix might look as follows:
Ltac iInternalFailMsg :=
idtac "Iris encountered an internal error! This is very bad!";
idtac "Please report a bug at https://gitlab.mpi-sws.org/iris/iris/-/issues ".
Ltac iExampleTac.
let H := constr:(I) in
iInternalFailMsg; fail "iTest: Something with" H "is off"
prepending iInternalFailMsg
to all such fail
statements.