Zulip Chat Archive

Stream: lean4

Topic: tactics should fail if they do nothing?


Scott Morrison (Nov 23 2022 at 14:34):

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 (Nov 23 2022 at 14:34):

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 (Nov 23 2022 at 14:40):

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

Jannis Limperg (Nov 23 2022 at 16:08):

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 (Nov 23 2022 at 16:19):

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 (Nov 23 2022 at 16:45):

tactics shouldn't be crashing?

Reid Barton (Nov 23 2022 at 16:46):

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

Johan Commelin (Nov 23 2022 at 16:51):

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 (Nov 23 2022 at 17:02):

tactics shouldn't be crashing?

True, programmers never make mistakes :upside_down:

Wojciech Nawrocki (Nov 23 2022 at 18:00):

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 (Nov 23 2022 at 18:10):

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 (Nov 23 2022 at 18:13):

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 (Nov 23 2022 at 20:59):

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 (Nov 23 2022 at 22:14):

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 (Nov 23 2022 at 22:14):

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


Last updated: Dec 20 2023 at 11:08 UTC