search

leanprover / reference-manual

Apache License 2.0
26 stars 3 forks source link

withMainContext #132

Open hrmacbeth opened 3 weeks ago

hrmacbeth commented 3 weeks ago

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 commented 3 weeks ago

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.