How to obtain a `LocalContext` from a `TacticInfo`?

Stream: lean4

[Scott Morrison]

Say I've explored an InfoTree and found a t : TacticInfo that I'm interested in, along with the enclosing ctx : ContextInfo. I'd like to pretty print one of the goals g ∈ t.goalsBefore.

I'd hope that I could write ctx.runMetaM {} (do ppExpr (← t.goalsBefore.head!.getType)).

However this prints something like: Subtype.restrict _uniq.6454 (fun x => _uniq.6455 x) _uniq.6457 _uniq.6456 _uniq.6458 = _uniq.6456 _uniq.6458.val, with all the local variables missing. This is perhaps not so surprising, as in the runMetaM call above I passed an empty {} : LocalContext.

Where can I find the relevant LocalContext? A TermInfo contains a LocalContext, but a TacticInfo doesn't.

(Apologies for the lack of #mwe; I can try to produce one if no one sees off the bat what I'm doing wrong.)

[Sebastian Ullrich]

The local context is part of the mvar context, see e.g. docs4#Lean.Elab.TacticInfo.format

[Kyle Miller]

You have to make sure to set the metavariable context too. Untested, but this should be close: Meta.withMCtx t.mctxBefore <| t.goalsBefore.head!.withContext <| do ppExpr (<- t.goalsBefore.head!.getType). (Don't forget the do, otherwise the arrow will be lifted out of the expression into a place where the contexts have not been set! This might not be a problem in this particular case, but this can make for some hard to debug issues.)

[Scott Morrison]

Thanks, got this working.