disable fail on no goals

Stream: lean4

[Aaron Liu]

Most tactics can fail with a message no goals to be solved. This can cause some issues, especially in automation (I have seen it 3 times now). Should there be a way to turn this off?

[Kyle Miller]

If you have examples of this happening, could you please share?

[Aaron Liu]

#lean4 > Cannot prove index is valid
#new members > Matrix inverse and group structure @ 💬
#lean4 > Creating a tactic @ 💬

[Mario Carneiro]

I don't think an option would help here. In automation, you need the fix to be local, and I don't see how set_option tactic.failOnNoGoals false in (tac1; tac2) is better than tac1 <;> tac2 which is what we would usually recommend in such a situation

[Kyle Miller]

There's one part of this that I've been considering modifying, and that's having autoParam tactics not run if their metavariable is solved for (or at least giving a better error than "no goals to be solved", for example give a hint to add (argName := _)).

[Aaron Liu]

Mario Carneiro said:

I don't think an option would help here. In automation, you need the fix to be local, and I don't see how set_option tactic.failOnNoGoals false in (tac1; tac2) is better than tac1 <;> tac2 which is what we would usually recommend in such a situation

Sometimes you have something more complicated than just tac1; tac2

[Kyle Miller]

Failing on no goals is the correct behavior, and I don't think having an option to turn it off makes much sense.

What does make sense to me are:

• observing that the issues appear to be with autoParams, so improve the autoParam experience by having the tactic runner first check if the goal has already been solved; it's something it really should have been checking anyway.
• use all_goals as a prefix if you're somehow in some other situation where you don't know if there is a goal or not.