Problem with `repeat'`

Stream: std4

[Scott Morrison]

I'm having a problem with repeat'. Here's the smallest minimisation I have so far:

import Std.Tactic.Basic

open Lean Elab Tactic Meta

def Lean.MVarId.assignFresh (mvarId : MVarId) : MetaM MVarId := do
  let mvarIdNew ← mkFreshExprMVar (← mvarId.getType)
  mvarId.assign mvarIdNew
  return mvarIdNew.mvarId!

elab "foo" : tactic => liftMetaTactic fun g => do _ ← g.assignFresh; throwError ""

example : False := by -- (kernel) declaration has metavariables '_example'
  repeat' foo

[Scott Morrison]

This also happens with g.assignFresh replaced by g.exFalso.

[Scott Morrison]

This is minimised from the even shorter:

import Mathlib.Tactic.Linarith

example : False := by -- (kernel) declaration has metavariables '_example'
  repeat' linarith

[Scott Morrison]

@Mario Carneiro, do you see what is wrong here? I think it must be repeat's fault.

[Mario Carneiro]

Your foo is breaking the contract that repeat' expects. Specifically, if you throw an exception, then repeat' will put the original goal back on the goal list, so it should not be assigned. If it is assigned then it will be pruned from the list, so in this example that means that mvarIdNew is dropped on the floor and you have an empty goal list even though there are metavariables remaining

[Scott Morrison]

Would it be okay to change repeat' so it rewinds the MetavarContext on an exception?

[Scott Morrison]

This seems like a nasty footgun (as evidenced by the repeat' linarith example).

[Mario Carneiro]

is it something that can be fixed in linarith?

[Scott Morrison]

But... but... where is the contract that says that failing tactics are responsible for rewinding all of their state? That's not a universal expectation, is it?

[Scott Morrison]

I thought this was unreasonable expectations on the part of repeat', not bad behaviour on the part of linarith.

[Mario Carneiro]

repeat' essentially uses a try catch block to catch exceptions in the inner function. This does not rewind the state by default

[Mario Carneiro]

it is not clear to me if rewinding the state is desirable in general

[Scott Morrison]

I'm worried that we have lots of tactics out there that error without rewinding the state, and repeat' is not going to be usable with any othem.

[Mario Carneiro]

fixed (I had to change observing to observing?... it is not good that such similarly sounding functions have this different behavior)

[Mario Carneiro]

std#305

[Scott Morrison]

Okay, and #7769 is the matching mathlib PR that makes sure linarith rolls back the state as well. Defence in depth!