indentation in infoview and pretty-printer

Stream: lean4

[Robin Carlier]

Consider the following

variable {C : Type}
infixr:80 " ≫ " => Function.comp
example (longname : C → C) (h : longname = id):
  longname ≫
    longname ≫
    longname ≫
    longname ≫
    longname ≫
    longname ≫
    longname ≫
    longname ≫
    longname ≫
    longname ≫
    longname ≫
    longname ≫
    longname = id := by
  /-
  ⊢ longname ≫
      longname ≫
        longname ≫
          longname ≫ longname ≫ longname ≫ longname ≫ longname ≫ longname ≫ longname ≫ longname ≫ longname ≫ longname =
    id
  -/
  sorry

In expressions where the number of compositions starts to get big enough (here, these are compositions, but this happens with any binary operator), the expressions in the infoview (coming from the pretty-printer representations I suppose? I’m not familiar with the internals at all) indent each new composition until the last line gets short enough.

I tend to work with mathlib's category theory library (which has the same notations as in my example), and I often run into big expressions with lots of compositions of terms with long names (especially when working with bicategories): I am losing a lot of screen space because of this indentation convention, and in extreme cases terms end up "squished" to the right and the resulting goal state is basically unreadable.

It would be much much more readable if they were to just align without adding an indentation degree each time (a bit like I did in the statement)

Is there any option/meta code/whatever I can use so that I can change this behavior (at least locally)?

[Kyle Miller]

If you redefine the syntax to have a ppDedent (which unfortunately requires avoiding notation and using syntax) it seems like it uses the indentation style you used in the source:

import Lean
variable {C : Type}
syntax:80 term:81 " ≫ " ppDedent(term:80) : term
macro_rules | `($a ≫ $b) => `(Function.comp $a $b)
@[app_unexpander Function.comp] def unexpandComp : Lean.PrettyPrinter.Unexpander
  | `($_ $a $b) => `($a ≫ $b)
  | _ => throw ()
example (longname : C → C) (h : longname = id):
  longname ≫
    longname ≫
    longname ≫
    longname ≫
    longname ≫
    longname ≫
    longname ≫
    longname ≫
    longname ≫
    longname ≫
    longname ≫
    longname ≫
    longname = id := by
  /-
  ⊢ longname ≫
      longname ≫
      longname ≫
      longname ≫ longname ≫ longname ≫ longname ≫ longname ≫ longname ≫ longname ≫ longname ≫ longname ≫ longname =
    id
  -/
  sorry

[Kyle Miller]

I wonder if there's any reason that pretty printing of binary operations shouldn't work this way in general?

[Robin Carlier]

Thanks @Kyle Miller ! This works for category theory as well!

import Mathlib.CategoryTheory.Category.Basic
open CategoryTheory
variable {C : Type} [Category C]
syntax (name := myComp) (priority := high) term:81 " ≫ " ppDedent(term:80) : term
macro_rules (kind := myComp) | `($a ≫ $b) => `(CategoryStruct.comp $a $b)
@[app_unexpander CategoryStruct.comp] def unexpandComp : Lean.PrettyPrinter.Unexpander
  | `($_ $a $b) => `($a ≫ $b)
  | _ => throw ()
example (a : C) (longname : a ⟶ a) (h : longname = 𝟙 a):
  longname ≫
    longname ≫
    longname ≫
    longname ≫
    longname ≫
    longname ≫
    longname ≫
    longname ≫
    longname ≫
    longname ≫
    longname ≫
    longname = 𝟙 _ := by
/-
⊢ longname ≫
    longname ≫
    longname ≫ longname ≫ longname ≫ longname ≫ longname ≫ longname ≫ longname ≫ longname ≫ longname ≫ longname =
  𝟙 a
-/
  sorry

[Joachim Breitner]

If you fix this for binary operations, please also for -> so that large types print prettier

[Eric Wieser]

Could we teach this to allow multiple lines with more than one item, rather than partitioning as [1, 1, 1, ..., n]?

[Robin Carlier]

I’ll try to find some time to open an issue on the lean4 repo about this this week, but no promises.

[Kyle Miller]

Here's a style question:

Do people normally write

  t1 +
    t2 +
    t3 +
    t4

or

  t1
    + t2
    + t3
    + t4

The second is what I personally do (both in Lean and in mathematical writing).

Does it depend on what kind of operator it is? I see Robin end each line with the composition operator (perhaps simply to mimic Lean?) but I probably would have written it as

  longname
    ≫ longname
    ≫ longname
    ≫ longname
    ≫ longname
    = id

[Ruben Van de Velde]

I tend to go for the first

[Chris Henson]

I will use whatever the future code formatter decides for me :)

(my non-joke answer is the second, because of annoyances in diffs, using #check, etc.)

[Robin Carlier]

I like the second (and used to prefer it), but Mathlib's conventions are to use the first, so I refrain myself from using it in code in practice.
In the best world there is an options to switch between the two in the pretty-printer

[Kyle Miller]

I'm sure this isn't quite right (my impression is that doing it robustly would require some actual support from the pretty printer), but here's an approximation/hack using pp syntax combinators that seems to do the trick:

import Mathlib.CategoryTheory.Category.Basic
open CategoryTheory
variable {C : Type} [Category C]
syntax (name := myComp) (priority := high) term:81 ppSpace ppRealGroup("≫" ppHardSpace ppDedent(term:80)) : term
macro_rules (kind := myComp) | `($a ≫ $b) => `(CategoryStruct.comp $a $b)
@[app_unexpander CategoryStruct.comp] def unexpandComp : Lean.PrettyPrinter.Unexpander
  | `($_ $a $b) => `($a ≫ $b)
  | _ => throw ()
example (a : C) (longname : a ⟶ a) (h : longname = 𝟙 a):
  longname ≫
    longname ≫
    longname ≫
    longname ≫
    longname ≫
    longname ≫
    longname ≫
    longname ≫
    longname ≫
    longname ≫
    longname ≫
    longname = 𝟙 _ := by
/-
⊢ longname
    ≫ longname
    ≫ longname ≫ longname ≫ longname ≫ longname ≫ longname ≫ longname ≫ longname ≫ longname ≫ longname ≫ longname =
  𝟙 a
-/
  sorry

Getting it to fill (printing more than one operator/term pair per line, per @Eric Wieser's suggestion) would require pretty printer support for terms with mixed operators. It's possible to get it to work with just a single operator at a time though using the following approach:

import Mathlib.CategoryTheory.Category.Basic
open CategoryTheory
variable {C : Type} [Category C]
syntax (name := myComp) (priority := high) term:81 (ppSpace ppRealGroup("≫" ppHardSpace term:81))+ : term
macro_rules (kind := myComp)
  | `($a:term $[≫ $bs:term]*) => show Lean.MacroM (Lean.TSyntax `term) from
    let args := a :: bs.pop.toList
    args.foldrM (init := bs[bs.size - 1]!) fun a (e : Lean.TSyntax `term) =>
      `(CategoryStruct.comp $a $e)
@[app_unexpander CategoryStruct.comp] def unexpandComp : Lean.PrettyPrinter.Unexpander
  | `($_ $a $b) =>
    match b with
    | `($b1 $[≫ $bs]*) => let bs' := #[b1] ++ bs; `($a $[≫ $bs']*)
    | _ => `($a ≫ $b)
  | _ => throw ()
example (a : C) (longname : a ⟶ a) (h : longname = 𝟙 a):
  longname ≫ longname ≫ longname ≫ longname ≫ longname
    ≫ longname ≫ longname ≫ longname ≫ longname ≫ longname
    ≫ longname ≫ longname ≫ longname ≫ longname ≫ longname
    ≫ longname ≫ longname ≫ longname ≫ longname ≫ longname
    ≫ longname ≫ longname ≫ longname ≫ longname ≫ longname
    ≫ longname ≫ longname ≫ longname ≫ longname ≫ longname = 𝟙 _ := by
/-
⊢ longname ≫ longname ≫ longname ≫ longname ≫ longname ≫ longname ≫ longname ≫ longname ≫ longname ≫ longname ≫ longname
    ≫ longname ≫ longname ≫ longname ≫ longname ≫ longname ≫ longname ≫ longname ≫ longname ≫ longname ≫ longname
    ≫ longname ≫ longname ≫ longname ≫ longname ≫ longname ≫ longname ≫ longname ≫ longname ≫ longname =
  𝟙 a
-/
  sorry

[Robin Arnez]

I guess the standard library style conventions might also be a good data point?

Splitting terms across multiple lines

[...]
When splitting at an infix operator, the operator goes at the end of the first line, not at the beginning of the second line. When splitting at an infix operator, you may or may not increase indentation depth, depending on what is more readable.

[Robin Arnez]

Ah, right Robin Carlier already mentioned that the first is the Mathlib convention, I guess Lean's standard library adopted that

[Max Nowak 🐉]

Random wild, probably awful, idea: what about a (->) syntax:

(->)
  (a : A)
  (b : B)
  C

[Eric Wieser]

Best I can do is

import Mathlib

#check
  beta% (· → ·)
    Nat
    Int