feat: rewrite the linter for spaces before semicolons in Lean #16532

grunweg · 2024-09-06T13:26:38Z

depends on: [Merged by Bors] - feat: rewrite the trailing whitespace linter in Lean #16334

…auto-fixes

There is an in-progress PR batteries to the same effect: when that PR lands, this linter can be removed. Both implement basically the same logic. This linter is consciously not rewritten as a syntax linter, as a fair number of mathlib contributors have their text editor configured to remove trailing whitespace when saving: with such configurations, in effect, the linter would only fire intermittently (such as, between keypresses), which is not helpful. Running this as a text-based linter in CI, which is auto-fixable, is far more helpful.

github-actions · 2024-09-06T13:27:21Z

PR summary cf9e63e260

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ semicolonLinter
+ trailingWhitespaceLinter
- line_endings_check(lines,

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

grunweg · 2024-11-21T16:02:06Z

Actually, this reveals a bug in the suggested auto-fix: while lake exe lint-style respects the linter exclusions, the auto-fix doesn't. Marking as awaiting-author.

github-actions · 2024-11-21T16:06:37Z

Mathlib/Tactic/Linter/TextBased.lean

@@ -56,6 +56,10 @@ inductive StyleError where
  | adaptationNote
  /-- A line ends with windows line endings (\r\n) instead of unix ones (\n). -/
  | windowsLineEnding
+  /-- A line contains trailing whitespace. -/
+  | trailingWhitespace
+  /-- A line contains the string " ;" -/


[lint-style (comment with "bot fix style" to have the bot commit all style suggestions)] _{reported by reviewdog 🐶}

Suggested change

/-- A line contains the string " ;" -/

/-- A line contains the string ";" -/

github-actions · 2024-11-21T16:06:37Z

Mathlib/Tactic/Linter/TextBased.lean

+  return (errors, if errors.size > 0 then some fixedLines else none)
+
+
+/-- Lint a collection of input strings for the substring " ;". -/


[lint-style (comment with "bot fix style" to have the bot commit all style suggestions)] _{reported by reviewdog 🐶}

Suggested change

/-- Lint a collection of input strings for the substring " ;". -/

/-- Lint a collection of input strings for the substring ";". -/

github-actions · 2024-11-21T16:06:37Z

Mathlib/Tactic/Linter/TextBased.lean

+    -- Future: also lint for a semicolon *not* followed by a space or ⟩.
+    if pos != line.endPos && line.get (line.prev pos) == ' ' then
+      errors := errors.push (StyleError.semicolon, idx + 1)
+      fixedLines := fixedLines.set! idx (line.replace " ;" ";")


[lint-style (comment with "bot fix style" to have the bot commit all style suggestions)] _{reported by reviewdog 🐶}

Suggested change

fixedLines := fixedLines.set! idx (line.replace " ;" ";")

fixedLines := fixedLines.set! idx (line.replace ";" ";")

kim-em · 2024-11-22T01:50:00Z

bors d+

mathlib-bors · 2024-11-22T01:50:02Z

✌️ grunweg can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

mathlib4-dependent-issues-bot · 2024-11-22T02:29:09Z

This PR/issue depends on:

~~[Merged by Bors] - feat: rewrite the trailing whitespace linter in Lean #16334~~
By Dependent Issues (🤖). Happy coding!

grunweg added 15 commits August 30, 2024 23:26

feat: rewrite the windows line endings linter

31afbee

chore: make text-based linters return the fixed lines, if any

59ea5e9

feat: auto-fix line ending warnings

f4c1436

feat: when the --fix is given, change the linted module according to …

6436ad3

…auto-fixes

chore: remove corresponding Python style linter

2900855

fix: actually detect line length thingies

8988620

Merge branch 'master' into MR-rewrite-lineending-linter

8ca28f3

Fix merge

4fa03af

Merge branch 'master' into MR-rewrite-lineending-linter

044cbbf

Review comments.

5196b7d

Merge branch 'master' into MR-rewrite-lineending-linter

4994d77

fix line numbers; better iteration over the array

34b6ef3

Tweaks.

81bfec2

Merge branch 'master' into MR-trailingWhitespaceLinter

5a7b317

grunweg added the t-linter Linter label Sep 6, 2024

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Sep 6, 2024

Small golf: use Array.zipWithIndex

8863151

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Sep 12, 2024

Merge branch 'master' into MR-trailingWhitespaceLinter

6ef05fb

grunweg mentioned this pull request Oct 31, 2024

[Merged by Bors] - chore(scripts): require all scripts to be documented in the README #14539

Closed

grunweg added 3 commits November 21, 2024 16:43

Merge branch 'master' into MR-trailingWhitespaceLinter

1099845

chore: also use zipWithIndex in the adaptationNoteLinter

cae8fab

feat: rewrite the linter for the string ' ;' in Lean

2f91482

grunweg force-pushed the MR-rewrite-semicolonlinter branch from 930f60f to 2f91482 Compare November 21, 2024 15:54

grunweg added awaiting-author A reviewer has asked the author a question or requested changes and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Nov 21, 2024

Tweak auto-fix and simplify the logic.

cf9e63e

github-actions bot reviewed Nov 21, 2024

View reviewed changes

leanprover-community-mathlib4-bot added delegated and removed awaiting-author A reviewer has asked the author a question or requested changes labels Nov 22, 2024

mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Nov 22, 2024

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 22, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: rewrite the linter for spaces before semicolons in Lean #16532

feat: rewrite the linter for spaces before semicolons in Lean #16532

grunweg commented Sep 6, 2024 •

edited by Command-Master

Loading

github-actions bot commented Sep 6, 2024 •

edited

Loading

Declarations diff

grunweg commented Nov 21, 2024

github-actions bot Nov 21, 2024

github-actions bot Nov 21, 2024

github-actions bot Nov 21, 2024

kim-em commented Nov 22, 2024

mathlib-bors bot commented Nov 22, 2024

mathlib4-dependent-issues-bot commented Nov 22, 2024

	/-- A line contains the string " ;" -/
	/-- A line contains the string ";" -/

		return (errors, if errors.size > 0 then some fixedLines else none)


		/-- Lint a collection of input strings for the substring " ;". -/

	fixedLines := fixedLines.set! idx (line.replace " ;" ";")
	fixedLines := fixedLines.set! idx (line.replace ";" ";")

feat: rewrite the linter for spaces before semicolons in Lean #16532

Are you sure you want to change the base?

feat: rewrite the linter for spaces before semicolons in Lean #16532

Conversation

grunweg commented Sep 6, 2024 • edited by Command-Master Loading

github-actions bot commented Sep 6, 2024 • edited Loading

PR summary cf9e63e260

Import changes for modified files

Declarations diff

grunweg commented Nov 21, 2024

github-actions bot Nov 21, 2024

Choose a reason for hiding this comment

github-actions bot Nov 21, 2024

Choose a reason for hiding this comment

github-actions bot Nov 21, 2024

Choose a reason for hiding this comment

kim-em commented Nov 22, 2024

mathlib-bors bot commented Nov 22, 2024

mathlib4-dependent-issues-bot commented Nov 22, 2024

grunweg commented Sep 6, 2024 •

edited by Command-Master

Loading

github-actions bot commented Sep 6, 2024 •

edited

Loading