Naive question: safety of tactics

Stream: lean4

[Siddhartha Gadgil]

I was trying to understang some of the source code, specifically liftMetaTactic and have a naive question - what goes wrong if we call this with a tactic that simply maps MVarId to return [], i.e., just declares no goals are left. Is such a function not well-defined for some reason? Or is it the responsibility of the tactic writer, and a failure will happen later?

Thanks.

[Mario Carneiro]

this will definitely not be caught at compile time if that's what you mean

[Siddhartha Gadgil]

Thanks. That is what I meant.

[Mario Carneiro]

You can do the same thing in lean 3 tactics. What happens is that you get no goals so it looks like you finished, but then you get a more low level error saying the tactic didn't actually produce a complete term like it was supposed to

[Mario Carneiro]

This is generally considered a bug in the tactic

[Siddhartha Gadgil]

Thanks. So I see it is the responsibility while writing a tactic to ensure that MVar is a consequence of the new metavariables returned, and that a proof of this has been added (to the local context?)

[Mario Carneiro]

You should ensure that the input MVar is either passed back out as a goal, or assigned to an expression which would be a complete term if all the mvars returned as goals are assigned to complete terms

[Siddhartha Gadgil]

What does _assign_ mean here?