tactic_code_action find the context after the execution of t

Stream: mathlib4

[yannis monbru]

Hi, i am doing some experiments with tactic_code_actions, (basically playing with the example of createCalc) which is printing a format version of the goal before the tactic is applied, but i would like to do similar stuff with the goal after the tactic is applied ( see mwe). However it turns out that the context (ctx variable) is not the good one to get a format of the goal after.
Does somebody know how to find the adapted context, or a way to fix this?

import Mathlib
import Batteries

namespace Batteries.CodeAction

open Lean Meta Elab Tactic Server RequestM CodeAction

@[tactic_code_action Lean.Parser.Tactic.dsimp]
def Suffices : TacticCodeAction := fun _params _snap ctx _stack node => do
  let .node (.ofTacticInfo info) _ := node | return #[]

  let eager := {
    title := s!"Clic"
    kind? := "quickfix"
  }
  let doc ← readDoc
  return #[{
    eager
    lazy? := some do
      let tacPos := doc.meta.text.utf8PosToLspPos info.stx.getPos?.get!
      let endPos := doc.meta.text.utf8PosToLspPos info.stx.getTailPos?.get!

      let goal := info.goalsAfter[0]!
      --let goal := info.goalsBefore[0]!

      -- here ctx is the context before applying the tactic not the tactic
      let goalFmt ← ctx.runMetaM  {} <| goal.withContext do ppExpr (← goal.getType)


      return { eager with
        edit? := some <|.ofTextEdit doc.versionedIdentifier
          { range := ⟨tacPos, endPos⟩, newText := s!"suffices {goalFmt} by dsimp;assumption" }
      }
  }]

@[simps]
def foo : ℕ × ℤ := (4, 2)

example : foo.1 = 5 := by
  dsimp
  -- i would like :
  --suffices 4 = 5 by dsimp;assumption
  sorry

[Patrick Massot]

@Mario Carneiro any idea?

[yannis monbru]

It turns out that one can get the context (of type ContextInfo) by doing (thank's @Paul Lezeau )
let newCtx := {ctx with mctx := info.mctxAfter}

[Damiano Testa]

I had not noticed this message, but there is also #12006 (from a very very long time ago).

[Damiano Testa]

Note that it is not a code action, but a Try this.