withMainContext

[hrmacbeth]

What question should the reference manual answer?

One of the most common tactic bugs (seen at least a dozen times in examples on Zulip or in Mathlib PRs) is a missing withMainContext. What is a context? How is the context determined by default, and how does this change if a tactic is wrapped in withMainContext?

Maybe you could include an example of a small tactic with this error, showing the classic behaviour which signals this bug (tactic mysteriously ignores variables/hypotheses/goals which were not present at the start of the problem), and then a fixed version of the tactic.

[david-christiansen]

Thanks, this is useful feedback! I don't plan to address the deep guts of tactic implementation until sometime next year, but this is a very good thing to keep in mind for it.