Overuse (?) of soft newlines in pretty-printer

Stream: lean4

[Jannis Limperg]

I've noticed a couple of situations where the pretty-printer uses soft newlines where I would have expected a hard newline. Example:

import Lean

open Lean

#eval show CoreM Unit from do
  let thm ← `(command|
    theorem foo : 1 = 1 := by
      have : 1 = 1 := by
        simp)
  logInfo $ ← PrettyPrinter.ppCommand thm

-- theorem foo : 1 = 1 := by have : 1 = 1 := by simp

@Kyle Miller do you consider this a bug that should be reported?

[Kyle Miller]

I think often people expect one-liner tactics to print in one line.

Are you suggesting newlines after one or both of these bys?

It looks like this might be for pretty printing the start of a proof script. I wonder if there should be a special tactic (let's call it HERE% for now) that formats itself as a blank line, and then you could have

  let thm ← `(command|
    theorem foo : 1 = 1 := by
      have : 1 = 1 := by
        simp
      HERE%)

[Jannis Limperg]

I would definitely expect a hard newline after the first by. Theorem with proof all on one line seems like it would be "wrong" more often than "right". Though if the goal is to mimic human style very closely, I guess you'd have to distinguish between atomic tactics (:= by simp) and non-atomic tactics (:= by have ... := by simp).

The second by seems debatable. I would prefer consistency, but I can see the case for concise one-liners.

The printing-only tactic hack is a nice idea! I'll add this to the tool that sparked this conversation.