feat: add withInstantiateMainGoal combinator to help spread the cos…

…t of mvar instantiation

Tactics/Common.lean

@@ -278,5 +278,36 @@ Unlike the standard `withMainContext`, `x` may live in a generic monad `m`. -/
 def withMainContext' (x : m α) : m α := do
   (← getMainGoal).withContext x
 
+variable {m} [Monad m] [MonadLiftT TacticM m] [MonadLiftT MetaM m]
+  [MonadTrace m] [MonadLiftT IO m] [MonadLiftT BaseIO m] [AddMessageContext m]
+  [MonadRef m] [MonadOptions m] [MonadAlwaysExcept ε m] [MonadMCtx m] in
+/--
+`withInstantiateMainGoal x` will replace the main goal with a fresh metavariable
+of the same type, run `x` to solve for the new main goal, and then
+assign the old goal with the instantiating of the new goal.
+
+This seems redundant, but allows us to spread out the cost of metavariable
+instantiation, and hopefully avoid some quadratic behaviour we've observed.
+-/
+def withInstantiateMainGoal (x : m α) : m α := do
+  let oldGoal ← getMainGoal
+  let newGoal ← @id (TacticM _) <| do
+    let newGoal ← mkFreshMVarId
+    let oldDecl ← oldGoal.getDecl
+    newGoal.modifyDecl (fun decl => { decl with
+      type := oldDecl.type
+      kind := oldDecl.kind
+      userName := oldDecl.userName
+      lctx := oldDecl.lctx
+      localInstances := oldDecl.localInstances
+    })
+    replaceMainGoal [newGoal]
+    pure newGoal
+  let a ← x
+  withTraceNode `Tactic.sym (fun _ => pure m!"instantiating goal")
+    (tag := "instantiateMVar") <| do
+      let _ ← oldGoal.assign (← instantiateMVars (Expr.mvar newGoal))
+  return a
+
 /-- An emoji to show that a tactic is processing at an intermediate step. -/
 def processingEmoji : String := "⚙️"

Tactics/Sym.lean

@@ -233,6 +233,7 @@ context `c`, returning the context for the next step in simulation. -/
 def sym1 (whileTac : TSyntax `tactic) : SymM Unit := do
   let stateNumber ← getCurrentStateNumber
   withTraceNode m!"(sym1): simulating step {stateNumber}" (tag:="sym1") <|
+  withInstantiateMainGoal <|
   withMainContext' do
     withVerboseTraceNode "verbose context" (tag := "infoDump") <| do
       traceSymContext
@@ -365,7 +366,8 @@ Hypotheses `h_err` and `h_sp` may be missing,
 in which case a new goal of the appropriate type will be added.
 The other hypotheses *must* be present,
 since we infer required information from their types. -/
-elab "sym_n" whileTac?:(sym_while)? n:num s:(sym_at)? : tactic => do
+elab "sym_n" whileTac?:(sym_while)? n:num s:(sym_at)? : tactic =>
+  withTraceNode "" (tag := "sym_n") <| do
   traceHeartbeats "initial heartbeats"
 
   let s ← s.mapM fun
@@ -383,7 +385,9 @@ elab "sym_n" whileTac?:(sym_while)? n:num s:(sym_at)? : tactic => do
         ))
 
   let c ← SymContext.fromMainContext s
-  SymM.run' c <| withMainContext' <|  do
+  SymM.run' c <|
+  withInstantiateMainGoal <|
+  withMainContext' <|  do
     -- Check pre-conditions
     assertStepTheoremsGenerated
     let n ← ensureAtMostRunSteps n.getNat