Using infotree holes and `lazyAssignment`

Stream: lean4

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

I am trying to use InfoState.lazyAssignment with async elaboration following the def elaborator. However, it seems that the info is not used by the server unless I put it in explicitly as opposed to using InfoTree.hole. This is surprising because the def elaborator doesn't seem to do that. What am I doing wrong here?

import Lean

open Lean Meta Elab Tactic Widget in
elab stx:"info_hole" : tactic => do
  let infoHole ← mkFreshMVarId
  let wi ← WidgetInstance.ofHash TryThis.tryThisWidget.javascriptHash (pure .null)
  let info := InfoTree.node (.ofUserWidgetInfo { wi with stx }) .empty
  modifyInfoState fun s => { s with
    -- widget shows up with this \/
    --trees := s.trees.push info
    trees := s.trees.push <| .hole infoHole
    lazyAssignment := s.lazyAssignment.insert infoHole (Task.pure info)
  }

example : True := by
  info_hole -- no widget here
  sorry

[Kyle Miller]

Huh, if you look at the infotrees, then they are correct and the widget appears.

#info_trees in
example : True := by
  info_hole -- no widget here
  sorry

[Kyle Miller]

But if you don't, then it's not there.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

It also works with the pre-parallel-elaboration assignment := s.assignment.insert infoHole info. It looks like InfoTree.visitM just ignores holes. Should it be doing that? Is there a missing InfoTree.instantiateMVars (or whatever it's called) somewhere?

[Kyle Miller]

There's a InfoState.substituteLazy function that's responsible for this, and either it's not being called, or maybe there's something subtle about nested lazy assignments?

[Kyle Miller]

You can see in docs#Lean.Elab.Tactic.InfoTrees.elabInfoTrees that substituteLazy is called again

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

It's also higher latency to do this on the entire tree; the server should only wait on tasks that it actually needs. It would be easier if infotrees maintained the invariant that subtrees are always syntactic subranges, though, which iirc they sometimes don't.

[Sebastian Ullrich]

Finer-grained forcing of lazy assignments in the server is TBD, the simple current implementation assumes there are no lazy holes on the tactic level