Debug mode for tactics

[Kaptch]

During the Iris workshop, it was brought up that if someone wants to apply LLMs to help with Iris proofs, it would be beneficial to have a verbose output mode. I haven't thought about the design, so we can discuss it here. Perhaps, one could add a flag that in case of errors makes tactics dump the Iris goal in a more structured way. Plus, it would be nice if the output can be used to state intermediate goals (that is, output contains a valid Entails statement).

If anyone has more ideas on what would be helpful, feel free to propose other ideas. I haven't used LLMs for any big scale things, so I am not sure what would be helpful or not.

Possibly, there can be also some structured summary of Iris tactics?

[markusdemedeiros]

As for the structured summary of the Iris tactics, is tactics.md insufficient?

[Kaptch]

I think probably it would be beneficial to have explicit Rocq->Lean translation both for patterns and tactics.
But I'm not sure, though, if my intuition is correct, so would be nice to have more opinions :)

[MackieLoeffel]

I asked Fable 5 yesterday to generate an updated tactics.md and here is the result: #462
Please add comments there if you have suggestions for improvements.