understanding the low level

Stream: new members

[Ping J]

if I need a deep understanding of Lean.Meta.Basic, do I have a better alternative than reading the code?

the language reference seem not to go into low-level details and i can't find another doc that does

[(deleted)]

have you read this https://leanprover-community.github.io/lean4-metaprogramming-book/

[Ping J]

Huỳnh Trần Khanh said:

have you read this https://leanprover-community.github.io/lean4-metaprogramming-book/

yes, i have. very educational
it more focuses on the utility of metaprogramming framework

[Ping J]

for e.g. i'm having trouble locating the definition/implementation of keywords by, and keyword tactic seem to point to an empty category and i cannot understand the implementation

[Niels Voss]

I think some of the key syntax objects are registered as builtins, which (I think, and I'm not completely sure of this) means that even though they are defined within Lean, they are defined within some past version of Lean and are thus accessible even when Lean doesn't import anything.

See for example docs#Lean.Parser.Term.byTactic and docs#Lean.Elab.Term.elabByTactic

[Ping J]

Niels Voss said:

See for example docs#Lean.Parser.Term.byTactic and docs#Lean.Elab.Term.elabByTactic

thx for pointing out! i guess the latter is indeed the direction i should be looking into

[Ping J]

i'm reading

/--
Creates a new metavariable of type `type` that will be synthesized using the tactic code.
The `tacticCode` syntax is the full `by ..` syntax.
-/
def mkTacticMVar (type : Expr) (tacticCode : Syntax) (kind : TacticMVarKind)
    (delayOnMVars := false) : TermElabM Expr := do
  if ← pure (debug.byAsSorry.get (← getOptions)) <&&> isProp type then
    withRef tacticCode <| mkLabeledSorry type false (unique := true)
  else
    let mvar ← mkFreshExprMVar type MetavarKind.syntheticOpaque
    let mvarId := mvar.mvarId!
    let ref ← getRef
    registerSyntheticMVar ref mvarId <| .tactic tacticCode (← saveContext) kind delayOnMVars
    return mvar

and am still quite lost. i think i'm confused mainly by oblivion of

1. how is the delay/postpone orchestrated
2. what is the code path from here to the code enabling e.g. tactic customization in metaprogramming