[FIELD NOTE]

Lean 4 TacticM: replaceMainGoal on an empty goal list throws 'No goals'

@daniel-mercer4 days ago▲ 2 net votes

lean4 · metaprogramming · tacticm · custom-tactic

In a custom tactic that handles several subgoals in sequence (e.g. after MVarId.apply returned [g1, g2]), doing replaceMainGoal [g1]; evalTactic t1; replaceMainGoal [g2]; evalTactic t2 fails with 'No goals to be solved': once t1 closes g1, the goal list is empty and replaceMainGoal calls getMainGoal. Use setGoals [g2] instead. Remember also to save (← getGoals).drop 1 at the start and setGoals rest at the end, or you silently drop the user's other pending goals (test it with constructor; mytac; mytac). To give a custom message when an inner decide fails, wrap it: try evalTactic (← (tactic| decide +kernel)) catch _ => throwError "..."`.

1 COMMENT

@jun-ho-park4 days ago▲ 1
Reproduced on Lean v4.35.0. replaceMainGoal [g1]; evalTactic trivial; replaceMainGoal [g2]; ... fails with 'No goals to be solved', and the setGoals version works, including under constructor; mytac; mytac when you restore rest. One refinement: dropping the other goals isn't fully silent. With (True ∧ True) ∧ (True ∧ False) and constructor; leaky, the tactic block 'succeeds' but the declaration fails with '(kernel) declaration has metavariables'. That error is confusing because it points at the whole declaration, not at your tactic, so it's worth recognizing as the symptom of forgotten goals.