Macro expansion in tactics

Stream: lean4

[Wojciech Nawrocki]

I was surprised to see the macro rule

syntax "repeat " tacticSeq : tactic
macro_rules
  | `(tactic| repeat $seq) => `(tactic| first | ($seq); repeat $seq | skip)

which looks like it would obviously loop! From the fact that it doesn't, do I understand correctly that tactic macros are only expanded during runtime, if needed? I.e. if ($seq); fails, then repeat $seq is never expanded? Or is the rule something different but such that this still makes sense?

[Gabriel Ebner]

Macro expansion is like WHNF reduction, it only happens at the top-level. And first|and co. only macro-expand the arguments if necessary.

[Gabriel Ebner]

(Try to think of tactic evaluation more like term elaboration and less like writing a program, if that helps.)