pretty-printing puzzle

Stream: lean4

[Damiano Testa]

Here is something that surprised me.

How do you think that the pretty-printer prints these?

#check s!""
#check s!"{1}"

Answer

import Lean.Elab.Command

/--
info: #check s!""
---
info: #check s! "{1}"
-/
#guard_msgs in
run_cmd
  let s1 ← `(#check s!"")
  let s2 ← `(#check s!"{1}")
  Lean.logInfo s1
  Lean.logInfo s2

[Mario Carneiro]

I guess this is because s! takes a term <|> interpolatedStr(term) and so they may be handled differently

[Thomas Zhu]

macro:max "mys!" interpStr:interpolatedStr(term) : term =>
  do interpStr.expandInterpolatedStr (← `(String)) (← `(toString))

run_cmd
  let s1 ← `(term| mys!"")
  let s2 ← `(term| mys!"{1}")
  Lean.logInfo s1
  Lean.logInfo s2

Output:

mys!""
mys! "{1}"

[Thomas Zhu]

Input:

syntax "a" interpolatedStr(term) : term
syntax "!" interpolatedStr(term) : term
run_meta
  let s1 ← `(term| a"{1}")
  let s2 ← `(term| !"{1}")
  Lean.logInfo s1
  Lean.logInfo s2

Output:

a "{1}"
!"{1}"

[Aaron Liu]

I guess s! is a valid identifier

[Thomas Zhu]

Is it something to do with docs#Lean.PrettyPrinter.Formatter.State.leadWordIdent ?

[Thomas Zhu]

I think it's this line https://github.com/leanprover/lean4/blob/7c3ca70e29a0806bd4bfc62eae7084bbaf1a303d/src/Lean/PrettyPrinter/Formatter.lean#L386

[Thomas Zhu]

syntax "t!" term : term
run_meta
  logInfo (← `(term| t! ""))
  logInfo (← `(term| t! fun _ => _))
  logInfo (← `(term| t! λ _ => _))
  logInfo (← `(term| t! 1))
  logInfo (← `(term| t! -1))
  logInfo (← `(term| t! _))

[Thomas Zhu]

t!fun, t!1, and t!_ are valid identifiers, so spaces are inserted

[Damiano Testa]

Thank you all for your comments! I do not know if I understand better or worse what is going on now. :upside_down:

[Damiano Testa]

Here is another:

#check let a := 0;0
#check let (a) := 0;0

Pretty printed

/--
info: let a := 0;
0
---
info: let(a) := 0;
0
-/
#guard_msgs in
run_cmd
  let a := Lean.mkIdent `a
  let s1 ← `(let $a := 0;0)
  let s2 ← `(let ($a) := 0;0)
  Lean.logInfo s1
  Lean.logInfo s2

[Thomas Zhu]

I think this is the same idea: leta would be seen as a single identifier, so a space is inserted

[Damiano Testa]

I agree, I think that the other is the weird one, though.

[Thomas Zhu]

I agree, I think what happens is that somehow the tokenFn consumes beyond s! in s!"{, or maybe it's some other corner case that I didn't identify

[Thomas Zhu]

(I don't have time to look into the details)

[Thomas Zhu]

maybe we can use ppSpace in let and noWs in s! to eliminate the differences in behavior

[Damiano Testa]

I agree that adding a ppSpace for let is probably a good solution. I am not so sure about noWs in the other case, though.

[Thomas Zhu]

I am not familiar with parsers in Lean, perhaps there is a much better solution

[Mario Carneiro]

noWs is not just a pretty printer thing, it makes it a parse error to add a space which we probably don't want

[Aaron Liu]

is there a ppNoWs?

[Mario Carneiro]

that's just the default

[Mario Carneiro]

spaces between tokens are never inserted unless they would be required by the lexer

[Damiano Testa]

Right now, I am developing a version of the commandStart that seems to be correctly identifying whitespace issues on the vast majority of mathlib.

[Damiano Testa]

The main nodes that I have to silence are tactics such as apply and replace that, when followed by ( get pretty-printed without a space.

[Mario Carneiro]

those are all pretty printer bugs

[Mario Carneiro]

people don't use ppSpace as much as they should

[Damiano Testa]

If this could be fixed, then I think that most of the rest of the issues would be actually undetermined, so there could be a linter for whitespace on virtually everything in mathlib.

[Damiano Testa]

Mario Carneiro said:

people don't use ppSpace as much as they should

I agree and it looks like that is the major obstacle for trusting the pretty-printer from being a formatter.

[Mario Carneiro]

well no, I think the high level layout algorithm is not optimal for a formatter

[Damiano Testa]

Ah, I keep forgetting: the linter trusts line-breaks in the source, but spaces in the pretty-printer.