Extra spaces in prettyprinted term

Stream: metaprogramming / tactics

[Leni Aniva]

What causes the extra spacing in this example?

#eval do
  let z ← Elab.Term.elabTerm (← `(term|λ (x : Nat) => x + 1)) .none
  let stx ← PrettyPrinter.delab z
  logInfo s!"{stx.raw.prettyPrint}"

which shows

 fun  x  =>  x   +   1

[Robin Arnez]

Syntax.prettyPrint just prints the raw text contained in stx, including all trailing whitespace which might've been caused by certain syntax quotations in the delaborator containing them. You probably want ← PrettyPrinter.formatTerm stx instead.

[Leni Aniva]

Robin Arnez said:

Syntax.prettyPrint just prints the raw text contained in stx, including all trailing whitespace which might've been caused by certain syntax quotations in the delaborator containing them. You probably want ← PrettyPrinter.formatTerm stx instead.

sometimes PrettyPrinter.format functions throw "format: uncaught backtrack exception". Is there a way to diagnose it?

[Eric Wieser]

#lean4 > format: uncaught backtrack exception @ 💬

[Leni Aniva]

Eric Wieser said:

#lean4 > format: uncaught backtrack exception @ 💬

In this case I'm not using custom syntax, but I figured it out and it was because of malformed objects going into the prettyprinter.

[Eric Wieser]

The issue there is about a syntax defined in mathlib, minimized to not mention it

[Leni Aniva]

Eric Wieser said:

The issue there is about a syntax defined in mathlib, minimized to not mention it

Ah I see, there doesn't seem to be a conclusive solution