Pretty Print without Instantiating MVar

Stream: lean4

[Yicheng Qian]

Is there a way to pretty-print an expression with metavariables left uninstantiated? For example, suppose there is an expression e = ?m, is there a way to let trace[Meta.debug] m!"{e}" output ?m even after we've instantiated the metavariable ?m?
I've tried using withNewMCtxDepth <| trace[Meta.debug] m!"{e}, but it doesn't work.
By the way, in version lean4:nightly-2022-11-19, trace[Meta.debug] m!"{e}" won't instantiate metavariables in e when pretty-printing. However, after updating to lean4:nightly-2023-02-03, the metavariables in e are instantiated.

[Jannis Limperg]

If this is for debugging, toString e should work. If you want real pretty-printing (rather than a textual representation of the raw Expr), I don't think there's any function that'll give you that.

The behaviour you saw in the November version was presumably a bug where someone forgot to instantiateMVars.

[Gabriel Ebner]

I think set_option pp.instantiateMVars false should do the job.

[Gabriel Ebner]

You can probably set the option on an expression by calling e.setOption `pp.instantiateMVars false

[Yicheng Qian]

Gabriel Ebner said:

I think set_option pp.instantiateMVars false should do the job.

This does not work for me (also that option is false by default in lean4:nightly-2023-02-03). Finally I used this:

def withoutMVarAssignments (m : MetaM α) := do
  let mctx ← getMCtx
  Meta.withMCtx {mctx with eAssignment := {}, lAssignment := {}} m