How to make linter happy with my line breaks?

Stream: mathlib4

[Judah Towery]

I have this definition statement:

def whiskerRight₂ {A₀ A₁ A₂ : F ↓ X} {p₀ p₁ : Hom₁ F X A₀ A₁} (α : Hom₂ F X p₀ p₁)
    (p₂ : Hom₁ F X A₁ A₂) : Hom₂ F X (comp₁ F X p₀ p₂) (comp₁ F X p₁ p₂) where

If I put it all on one line, the linter complains that it is more than 100 characters. If I try to add a line break after the :, it is still more than 100 characters. When I try to line break as currently, the linter complains with:

remove line break in the source

This part of the code
  'p₁)
   '
should be written as
  'p₁) (p₂ :'

I also tried line breaking every assumption {} and () into its own line and got multiple of these 'remove line break in the source' complaints. What's the correct way to get it to stop complaining here?

[Kevin Buzzard]

What you've posted looks fine to me. I can't reproduce the error you're seeing -- can you make a #mwe ? What is the down-arrow?

[Judah Towery]

Kevin Buzzard said:

What you've posted looks fine to me. I can't reproduce the error you're seeing -- can you make a #mwe ? What is the down-arrow?

Sure:

import Mathlib.CategoryTheory.Bicategory.Functor.Lax

namespace CategoryTheory

open Category Bicategory

universe w₁ w₂ v₁ v₂

namespace LaxSlice

variable {B C : Type*} [Bicategory.{w₁, v₁} B] [Bicategory.{w₂, v₂} C]

variable (F : B ⥤ᴸ C) (X : C)

@[ext]
structure Obj where
  A : B
  f : F.obj A ⟶ X

scoped notation F " ↓ " X => Obj F X

@[ext]
structure Hom₁ (A₀ A₁ : F ↓ X) where
  p : A₀.A ⟶ A₁.A
  θ : A₀.f ⟶ F.map p ≫ A₁.f

@[ext]
structure Hom₂ {A₀ A₁ : F ↓ X} (p₀ : Hom₁ F X A₀ A₁) (p₁ : Hom₁ F X A₀ A₁) where
  α : p₀.p ⟶ p₁.p
  icc : p₀.θ ≫ (F.map₂ α ▷ A₁.f) = p₁.θ

@[simps]
def comp₁ {A₀ A₁ A₂ : F ↓ X} (p₀ : Hom₁ F X A₀ A₁) (p₁ : Hom₁ F X A₁ A₂) : Hom₁ F X A₀ A₂ where
  p := p₀.p ≫ p₁.p
  θ := p₀.θ ≫ (F.map p₀.p ◁ p₁.θ) ≫ (α_ (F.map p₀.p) (F.map p₁.p) A₂.f).inv
       ≫ (F.mapComp p₀.p p₁.p ▷ A₂.f)

@[simps]
def whiskerLeft₂ {A₀ A₁ A₂ : F ↓ X} (p₀ : Hom₁ F X A₀ A₁) {p₁ p₂ : Hom₁ F X A₁ A₂}
    (α : Hom₂ F X p₁ p₂) : Hom₂ F X (comp₁ F X p₀ p₁) (comp₁ F X p₀ p₂) where
  α := p₀.p ◁ α.α
  icc := by dsimp
            simp [←comp_whiskerRight, ←α.icc]
            rw [whisker_assoc_symm]
            simp

@[simps]
def whiskerRight₂ {A₀ A₁ A₂ : F ↓ X} {p₀ p₁ : Hom₁ F X A₀ A₁} (α : Hom₂ F X p₀ p₁)
    (p₂ : Hom₁ F X A₁ A₂) : Hom₂ F X (comp₁ F X p₀ p₂) (comp₁ F X p₁ p₂) where
  α := α.α ▷ p₂.p
  icc := by dsimp
            simp [←α.icc]
            rw [←assoc (F.map₂ α.α ▷ A₁.f), ←whisker_exchange]
            simp [←comp_whiskerRight]

Strangely enough, I just realized that it's fine with whiskerLeft_2? Maybe I'm doing something really silly.

[Michael Rothgang]

Does your line include trailing whitespace? If so, just remove it and the linter may already be fine. :-)

[Michael Rothgang]

CC @Damiano Testa The commandStart linter seems to have a bug in case the pretty-printed declaration is longer than 100 characters. (I'm happy to review a fix, but cannot say that I'll have time to fix it.)

[Judah Towery]

Michael Rothgang said:

Does your line include trailing whitespace? If so, just remove it and the linter may already be fine. :-)

That was it. There was indeed a whitespace at the end of the whiskerLeft_2 line. Thank you!

[Damiano Testa]

Michael, do you have an example for what the bug is? The line breaks in the pretty-printed text should be ignored by the commandStart linter.

[Notification Bot]

This topic was moved here from #lean4 > How to make linter happy with my line breaks? by Michael Rothgang.

[Michael Rothgang]

Ah right... count me as "I got confused by the error message" then. (I've seen this one before, and been confused by it before. But if I forget in between subsequent times, I can get confused again :-))

[Michael Rothgang]

To me, the error suggests "remove the line break", which (in this case) is very much not desirable.

[Damiano Testa]

The immediate reason why the linter says this, is that the "pretty printed with line breaks removed" text matches the user provided one up to the space. Then, the pretty printed one has a non-line-break character, while the user text contains a line break. Hence, it suggests to remove the line break.

[Damiano Testa]

Maybe there could be an earlier mechanism that flags "spaces before line breaks", but this is not what the code currently does.