MessageData.ofPPFormat

Stream: Is there code for X?

[Joachim Breitner]

It seems that ofPPFormat can be used to create a MessageData „lazily“. I expect this would be very useful in tactic code of the form

throwError m!"foo bar {← baz}"

where baz : MetaM MessageData is a possibly expensive operation, and you don’t want to run it unless someone really looks at the message, so that try tac will not spend time assembling the error message.

But I don’t quite understand the plumbing here. Can one write a

lazyMessageData : MetaM MessageData → MessageData

or

lazyMessageData : MetaM MessageData → MetaM MessageData

somehow?

[Joachim Breitner]

Here is a first attempt, although I expect it loses the ability to hover…

def _root_.Lean.MessageData.thunk (f : Unit → MessageData) : MessageData :=
  .ofPPFormat <| { pp := fun
    | .some ppctx => do
      let msg := f ()
      msg.formatAux
        {currNamespace := ppctx.currNamespace, openDecls := ppctx.openDecls}
        (some {env := ppctx.env, mctx := ppctx.mctx, lctx := ppctx.lctx, opts := ppctx.opts})
    | .none => do
      let msg := f ()
      msg.format}

It seems hard to use ofPPformat for this without losing the info hover.

Let’s try adding a constructor .thunk : Thunk MessageData → MessageData… that works ok if the delayed code is pure, until you need to do MetaM stuff lazily, thenThunk is too restrictive, but .thunk : IO MessageData → MessageData fails inductive can’t recurse through IO, it seems… oh wey.

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

Here is my attempt:

import Lean
open Lean Elab Meta Term Command

def lazyMessageData (mx : MetaM MessageData) : MetaM MessageData := do
  let metaCtx ← readThe Meta.Context
  let metaSt ← getThe Meta.State
  let coreCtx ← readThe Core.Context
  let coreSt ← getThe Core.State
  let m := MessageData.ofPPFormat {
    pp := fun _ => do
      let (m, _) ←
        (mx >>= addMessageContextFull)
          |>.run' metaCtx metaSt
          |>.toIO coreCtx coreSt
      MessageData.format m
    }
  return m

elab "#test" t:term : command => do
  Command.liftTermElabM do
    let t ← elabTerm t none
    let m ← lazyMessageData (return m!"lazy: {t}")
    logInfo m
    logInfo m!"eager: {t}"


#test 42

You are right that it loses hovers. I am not entirely sure, but I'd say this is a bug. Perhaps in msgToInteractiveAux?

[Eric Wieser]

Is this "save all the state for a callback" what docs#control is for?

[Joachim Breitner]

Thanks @Wojciech Nawrocki! I am playing around with something similar in https://github.com/leanprover/lean4/pull/3234 now.

@Eric Wieser I thought so, but couldn't get it to work. Maybe we don’t have the necessary instances to go from MetaM to IO?