Zulip Chat Archive

Stream: CSLib

Topic: Weekly linting log

github mathlib4 bot (Dec 15 2025 at 05:10):

CSLib weekly lint run completed (d3d8a37).

Summary:

Warnings: 1

Chris Henson (Dec 15 2025 at 05:14):

@Jesse Alama The table is missing here, could you take a look when you get a chance? Thanks!

Jesse Alama (Dec 15 2025 at 13:05):

Chris Henson said:

Jesse Alama The table is missing here, could you take a look when you get a chance? Thanks!

I've done some tweaking here: https://github.com/leanprover/cslib/pull/221 . At first, I had a Bash script but reformulated it as a Python script, since it was getting a bit bulky.

github mathlib4 bot (Dec 17 2025 at 04:55):

CSLib weekly lint run completed (6b1264e).

Summary:

Warnings: 2

github mathlib4 bot (Dec 17 2025 at 09:36):

CSLib weekly lint run completed (c3be9f2).

Summary:

Warnings: 2

github mathlib4 bot (Dec 17 2025 at 10:19):

CSLib weekly lint run completed (aa7d978).
Warnings: 2

Lint message counts

	Message
1	'simp only [addHist]; grind' can be replaced with 'grind'
1	'grw [ih1, ih2]; grind' can be replaced with 'grind'

Chris Henson (Dec 17 2025 at 10:21):

@Jesse Alama Looks good, thanks for your patience with my repeated misunderstandings!

Jesse Alama (Dec 17 2025 at 10:41):

No problem! Happy to help out.

github mathlib4 bot (Dec 22 2025 at 05:11):

CSLib weekly lint run completed (6b7be4b).
Warnings: 2

Lint message counts

	Message
1	'simp only [addHist]; grind' can be replaced with 'grind'
1	'grw [ih1, ih2]; grind' can be replaced with 'grind'

github mathlib4 bot (Dec 29 2025 at 05:15):

CSLib weekly lint run completed (d6a1e29).
Warnings: 1

Lint message counts

	Message
1	'use t1'; grind' can be replaced with 'grind'

github mathlib4 bot (Jan 05 2026 at 05:19):

CSLib weekly lint run completed (ff529e0).
Warnings: 1

Lint message counts

	Message
1	'use t1'; grind' can be replaced with 'grind'

github mathlib4 bot (Jan 12 2026 at 05:15):

CSLib weekly lint run completed (b55a607).
Warnings: 3

Lint message counts

	Message
1	'use t1'; grind' can be replaced with 'grind'
1	'use s, t; grind' can be replaced with 'grind'
1	'use s, t'; grind' can be replaced with 'grind'

github mathlib4 bot (Jan 19 2026 at 05:17):

CSLib weekly lint run completed (02e2a23).
Build completed without lint messages.

github mathlib4 bot (Jan 26 2026 at 05:18):

CSLib weekly lint run completed (d69fa7d).
Warnings: 1

Lint message counts

	Message
1	'use m + k; grind' can be replaced with 'grind'

github mathlib4 bot (Feb 02 2026 at 05:35):

CSLib weekly lint run completed (5e1873f).
Warnings: 3

Lint message counts

	Message
1	'use μs; grind' can be replaced with 'grind'
1	'use m + k; grind' can be replaced with 'grind'
1	'have : L'.app R ↠βᶠ L'.app R' := by grind; grind' can be replaced with 'grind'

github mathlib4 bot (Feb 09 2026 at 05:35):

CSLib weekly lint run completed (f0d87b6).
Warnings: 3

Lint message counts

	Message
1	'use μs; grind' can be replaced with 'grind'
1	'use m + k; grind' can be replaced with 'grind'
1	'have : L'.app R ↠βᶠ L'.app R' := by grind; grind' can be replaced with 'grind'

Chris Henson (Feb 09 2026 at 05:39):

These are addressed in cslib#312

github mathlib4 bot (Feb 16 2026 at 05:36):

CSLib weekly lint run completed (939bd13).
Warnings: 2

Lint message counts

github mathlib4 bot (Feb 23 2026 at 05:34):

CSLib weekly lint run completed (e448602).
Warnings: 3

Lint message counts

	Message
1	'use ss[μs1.length]'(by grind); grind' can be replaced with 'grind'
1	'use r; grind' can be replaced with 'grind'
1	'left; grind' can be replaced with 'grind'

Chris Henson (Feb 23 2026 at 07:48):

These are addressed in cslib#363

Last updated: Feb 28 2026 at 14:05 UTC