tactics should fail if they do nothing?

Stream: lean4

[Scott Morrison]

I know this has been discussed before, but I'm not sure that a decision was reached. In Lean 3 we had the convention that tactics should fail rather than succeed having achieved nothing. In particular both ext and simp had this behaviour, and in both cases they have changed in Lean 4.

[Scott Morrison]

I would love to return to the convention that tactics should fail. I think it's easier for humans, and easier for writing more complicated tactics that use these as building blocks.

[Scott Morrison]

The fix for ext would be very easy: https://github.com/leanprover/std4/pull/33.

[Jannis Limperg]

Yes please! Any search tactic generally wants to treat "no-op" as "failure", and it's much easier to turn a failure into a no-op than to check whether a success was in fact a no-op.

[Eric Wieser]

and it's much easier to turn a failure into a no-op

What if you want to distinguish "this tactic found nothing to match against" vs "this tactic crashed while processing the thing it matched against". I think failure on no-op is good for interactive tactics, but probably a bad idea for non-interactive tactics

[Scott Morrison]

tactics shouldn't be crashing?

[Reid Barton]

Noninteractive tactics could return a result Option whatever--but I assume the original message was talking about interactive tactics.

[Johan Commelin]

Scott Morrison said:

I would love to return to the convention that tactics should fail. I think it's easier for humans, and easier for writing more complicated tactics that use these as building blocks.

Continuing Reid's line of thought: Would it be fair to say that complicated tactics should generally use non-interactive tactics as building blocks?

[Eric Wieser]

tactics shouldn't be crashing?

True, programmers never make mistakes :upside_down:

[Wojciech Nawrocki]

Johan Commelin said:

Scott Morrison said:

I would love to return to the convention that tactics should fail. I think it's easier for humans, and easier for writing more complicated tactics that use these as building blocks.

Continuing Reid's line of thought: Would it be fair to say that complicated tactics should generally use non-interactive tactics as building blocks?

:+1: on this, and ideally the non-interactive variants return information about the status rather than just Unit. It is more readable to do something with a TacticM Bool or TacticM (Option _) than to call a TacticM Unit and use try-catch for control flow.

[Matthew Ballard]

How about throwing a error warning on a no-op for an interactive tactic? I want _something_ to tell me about a no-op but can understand the argument that a no-op is not failure.

[Scott Morrison]

I think we're in furious agreement that interactive tactics should fail rather than no-op, and non-interactive tactic may fail if they find nothing to do, but it's generally more useful to return something.

[Andrés Goens]

as a workaround, while not as good as having more useful return types, one thing you can do is something like a progress tactic that fails if no progress is made. We used a very crude version with @Fehr Mathieu when he was having trouble with repeat on tactics that ended being no-ops taking very long

elab  "progress " tac:tactic : tactic => do
    let goal ← getMainTarget
    (← getMainGoal).withContext do
     let lctx <- Lean.getLCtx
     evalTactic tac
     (← getMainGoal).withContext do
       let lctx' <- Lean.getLCtx
       let goal' ← getMainTarget
       let lctxDeclExprs := lctx.decls.toArray.map (Option.map Lean.LocalDecl.type)
       let lctx'DeclExprs := lctx'.decls.toArray.map (Option.map Lean.LocalDecl.type)
       if goal == goal' && lctxDeclExprs == lctx'DeclExprs then
         throwError "no progress made{(← getMainGoal).name}"

I'm sure this is not ideal, but it did seem to work for simple cases

[Eric Wieser]

That certainly takes the burden off tactics to try and track whether they had any effect, but presumably is less efficient as a result

[Eric Wieser]

But I guess progress would also fail on rw [foo, <-foo], which is probably a more useful behavior anyway