Migrating my custom tactic library from Lean 3

Stream: lean4

[Tsuru]

Lean 3 allows users to define some custom tactic monad and use it instead. Especially, begin[xxx] ... end blocks use tactics not from tactic.interactive but from xxx.interactive, making it easy to switch between different sets of tactics.
I learned this in https://leanprover-community.github.io/archive/stream/113488-general/topic/no.20lean.20messages.20output.20in.20hacked.20mode.html and (if necessary) my own code is
https://github.com/ge9/ntac/blob/c34eceeeaee6957f716874a5482ae23be94bbab1/src/ntac/ntac.lean#LL56C2-L56C3 .
Now I'm wondering how to implement this in Lean4. Any help would be appreciated!

[Floris van Doorn]

Metaprogramming in Lean 4 is a good place to start to learn: https://github.com/arthurpaulino/lean4-metaprogramming-book

[Tsuru]

Now I have suceeded in this.
First, define the custom tactic monad, and provide conversion functions and a required instance definition for it.

abbrev NTacticM := StateT My_State TacticM
abbrev NTactic  := Syntax → NTacticM Unit

def mylift {α} (m: TacticM α) : NTacticM α := fun x => do let res ← m; return (res, x)
def mylift_inv {α} (m: NTacticM α) : TacticM α := do let res ← m 0; return res.fst

instance [Monad m] [MonadRecDepth m] : MonadRecDepth (StateT α m) where
  withRecDepth d x := fun ctx => MonadRecDepth.withRecDepth d (x ctx)
  getRecDepth      := fun n => do let r ←  MonadRecDepth.getRecDepth; return (r, n)
  getMaxRecDepth   := fun n => do let r ←  MonadRecDepth.getMaxRecDepth; return (r, n)

Then I copied two definitions from the standard library and modified like this, to use the attribute attr_ntac_tactic instead of the existing tactic. (this is highly undocumented and I don't know its validity, but it's working)

unsafe def mkNTacticAttribute : IO (KeyedDeclsAttribute NTactic) :=
  mkElabAttribute NTactic `builtin_attr_ntac_tactic `attr_ntac_tactic `Ntac.Parser.Tactic `Ntac.Elab.Tactic.NTactic "ntac_tactic" `Ntac.Elab.Tactic.tacticElabAttribute

@[init mkNTacticAttribute] opaque tacticElabAttribute : KeyedDeclsAttribute NTactic

Then I redefined many existing parser and elab/eval functions, including byTactic, elabByTactic, tacticSeq, evalTacticSeq, tacticParser, evalTactic.
I modified tacticParser to accept both existing tactics and my custom ntac_tactics. (ntac_tactic is prioritized)

@[inline] def ntac_tacticParser (rbp : Nat := 0) : Parser :=
  (categoryParser `ntac_tactic rbp)  <|> (categoryParser `tactic rbp)

Now I can add custom tactic. This is custom exact tactic that imitates the default exact tactic, with a custom message.

syntax (name := ntac_exact) "exact " term : ntac_tactic
@[attr_ntac_tactic ntac_exact] def evalMyExact : Ntac.Elab.Tactic.NTactic := fun stx => do
  Lean.logInfo "this is my exact"
  Ntac.Elab.Tactic.mylift $ Lean.Elab.Tactic.evalTactic (stx.setKind `Lean.Parser.Tactic.exact)

I'll share the whole code at GitHub in the future, or soon if requested.