Meta.synthInstance.answer not registered

Stream: lean4

[Matthew Ballard]

In docs#Lean.Meta.SynthInstance.addAnswer, there is a trace for Meta.synthInstance.answer

def addAnswer (cNode : ConsumerNode) : SynthM Unit := do
  withMCtx cNode.mctx do
  if cNode.size ≥ (← read).maxResultSize then
      trace[Meta.synthInstance.answer] "{crossEmoji} {← instantiateMVars (← inferType cNode.mvar)}{Format.line}(size: {cNode.size} ≥ {(← read).maxResultSize})"
  else
    withTraceNode `Meta.synthInstance.answer
      (fun _ => return m!"{checkEmoji} {← instantiateMVars (← inferType cNode.mvar)}") do
    let answer ← mkAnswer cNode
    -- Remark: `answer` does not contain assignable or assigned metavariables.
    let key := cNode.key
    let entry ← getEntry key
    if isNewAnswer entry.answers answer then
      let newEntry := { entry with answers := entry.answers.push answer }
      modify fun s => { s with tableEntries := s.tableEntries.insert key newEntry }
      entry.waiters.forM (wakeUp answer)

but it is not registered at the bottom of the file.

Should this be Meta.synthInstance.newAnswer or should it be registered?

[Matthew Ballard]

lean#3373

[Thomas Murrills]

I was curious about other possible unregistered trace classes in core, and with a couple greps found the following trace classes which are used but not registered ("used" meaning trace[class.name] or withTraceNode `class.name, though except for Meta.synthInstance.answer, all cases happened to be of the former form)

Lean/PrettyPrinter/Delaborator/Basic.lean: PrettyPrinter.delab.input
Lean/Meta/Tactic/Simp/SimpAll.lean: Meta.Tactic.simp.all
Lean/Meta/DecLevel.lean: Meta.isLevelDefEq.step
Lean/Meta/SizeOf.lean: Meta.sizeOf.minor
Lean/Meta/SizeOf.lean: Meta.sizeOf.minor.step
Lean/Meta/SizeOf.lean: Meta.sizeOf.aux
Lean/Meta/SizeOf.lean: Meta.sizeOf.loop
Lean/Elab/StructInst.lean: Elab.struct.modifyOp
Lean/Elab/Quotation.lean: Elab.match_syntax.onMatch
Lean/Elab/Term.lean: Elab.implicitForall
Lean/Elab/SyntheticMVars.lean: Elab.defaultInstance
Lean/Elab/MutualDef.lean: Elab.definition.mkClosure
Lean/Elab/Binders.lean: Elab.autoParam
Lean/Elab/Binders.lean: Elab.let.decl

[Eric Wieser]

Is it a feature that trace[oops.i.forgot.to.register.this] is legal?

[Jovan Gerbscheid]

Any progress on this? In the meantime, Meta.synthInstance.answer has been added lean4#4151.

[Jovan Gerbscheid]

Eric Wieser said:

Is it a feature that trace[oops.i.forgot.to.register.this] is legal?

trace[...] is a macro that turns the part in square brackets into a Name. With the present implementation it is a bit tricky to check whether this name is registered or not. And often the registering happens after using the trace.

[Mario Carneiro]

I don't see anything in principle preventing us from checking that at compile time, although of course several trace registrations will have to be moved up first

[Jovan Gerbscheid]

Note also that it needs to play well with do-notation: we want the ← actions inside the trace[...] to not leak outside, so that they are only run when the trace option is set to true.

[Mario Carneiro]

I believe it already does this

[Jovan Gerbscheid]

Yes it does