Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Tracking PR] feat: rewrite most style linters in Lean #13199

Draft
wants to merge 64 commits into
base: master
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
64 commits
Select commit Hold shift + click to select a range
e70340d
feat: rewrite set_option style linter in lean
grunweg May 15, 2024
fb4aa88
Fix setOption linter in tests: mostly disable it; in one instance, on…
grunweg May 15, 2024
0e976bc
wip: lint on broad imports
grunweg May 15, 2024
b71c570
fixup! remove ERR_OPT branch which was unreachable
grunweg May 15, 2024
6c0bd51
wip
grunweg May 15, 2024
baf9aed
Checkpoint for this afternoon: reading Mathlib.lean works, linting fo…
grunweg May 17, 2024
b7641e3
Nicer and slightly stronger algorithm for validating the copyright. F…
grunweg May 17, 2024
7f93dac
Add file for text-based linters, and port output machinery.
grunweg May 25, 2024
5e4a10b
Port the first linter: line length.
grunweg May 25, 2024
eb4710f
Support multiple linters.
grunweg May 25, 2024
a1bb136
Style tweaks.
grunweg May 25, 2024
84a51e4
Add text-based linter for Mathlib.Tactic imports: I can delete my old…
grunweg May 25, 2024
8c28e13
Rewrite copyright header and author line linter.
grunweg May 25, 2024
8c1b35e
Synchronize my linter to the Python script.
grunweg May 25, 2024
6288545
More types: no idea if this is better.
grunweg May 25, 2024
4b50fbe
Remove now-rewritten python style lints.
grunweg May 25, 2024
a57174d
Use \N notation: the import is extremely cheap.
grunweg May 25, 2024
ac946ec
Port most remaining formatting linters to Lean.
grunweg May 25, 2024
6d70611
Port the 'isolated by' logic.
grunweg May 25, 2024
b005789
Testing my linters: with the author line logic.
grunweg May 25, 2024
2d3babf
Add imports to Mathlib.lean; re-instate line length Python linter.
grunweg May 25, 2024
1d8e0db
Small hack: fix one overly long line --- so I don't need
grunweg May 25, 2024
6fc9ce0
Add documentation; slightly minimize imports.
grunweg May 25, 2024
ef10da6
Rewrite the line endings check in Lean.
grunweg May 25, 2024
fef2bbd
style: remove last isolated where
grunweg May 25, 2024
18e9c21
Upgrade the 'isolated by' lint; add an 'isolated where' lint.
grunweg May 25, 2024
2e47f49
fix: do not lint import-only files
grunweg May 25, 2024
a5d44dc
Pass ignored errors through the script.
grunweg May 25, 2024
2a74d28
Port linter of too large files.
grunweg May 25, 2024
31847cf
Add line numbers to "line too length" error.
grunweg May 25, 2024
ae5f5fc
wip: mostly parse the style-exceptions:
grunweg May 25, 2024
8fb41cf
Remove last ERR_LIN style exception: the linter already
grunweg May 25, 2024
44a0536
HACK: comment out most of the script... something broke it.
grunweg May 25, 2024
b0a225b
Finish parsing the style exceptions.
grunweg May 25, 2024
d7f2317
Fix silly bugs: the basic script works!
grunweg May 25, 2024
5fb4a48
chore: ensure the first line of each copyright header has all periods…
grunweg May 25, 2024
9eb0b54
chore: copyright headers, uniformise copyright symbol
grunweg May 25, 2024
1a42b8c
Normalise a few more copyright headers.
grunweg May 25, 2024
05c51f3
temp: notes when gauging the performance
grunweg May 25, 2024
64394d4
perf: optimise check_line_length
grunweg May 25, 2024
43bbb7d
perf: optimise checking for misc formatting
grunweg May 25, 2024
efd7876
perf: optimise line ending checking
grunweg May 25, 2024
08994aa
Find the right size exception for each module; add some documentation.
grunweg May 25, 2024
a088785
Found the culprit: the semicolon check is abyssimal.
grunweg May 25, 2024
3bf1817
Remove large files check from lint-style.py.
grunweg May 25, 2024
1c28bef
Merge branch 'master' into MR-rewrite-more-style-linters
grunweg May 25, 2024
eef8612
Merge branch 'master' into MR-rewrite-more-style-linters
grunweg May 25, 2024
4d7c414
Move style exception parsing next to formatting of errors.
grunweg May 26, 2024
2aa8c7b
Use snakeCase for method names; I think this matches the naming conve…
grunweg May 26, 2024
1c464f5
Also lint Archive and Counterexamples.
grunweg May 26, 2024
0cee789
Normalise error contexts for comparing them:
grunweg May 26, 2024
052b0fd
For now, add a style-exceptions-new.txt file with style exceptions sp…
grunweg May 26, 2024
d5e7e6c
Use array literals for initialising arrays,
grunweg May 26, 2024
5f7cac3
wip: rewrite update_style_exceptions as a Lean executable
grunweg May 26, 2024
cb91d70
Use xargs instead: much better, now finishes within one second. Good …
grunweg May 26, 2024
a9ad582
Compile the linter (as opposed to interpreting it): *much* faster.
grunweg May 26, 2024
a48b16d
Remove supportInterpreter = true: this is not needed for my script.
grunweg May 27, 2024
7084023
Return the number of files with errors as exit code.
grunweg May 27, 2024
660ea06
Return the number of files with errors as exit code.
grunweg May 27, 2024
5ab09f0
revert head, is badof files with errors as exit code."
grunweg May 27, 2024
6f5a3f2
Run the new linter in the mathlib build workflow.
grunweg May 27, 2024
12960f7
Merge branch 'master' into MR-rewrite-more-style-linters
grunweg May 27, 2024
38b96fc
Make the semicolon check not complain about itself.
grunweg May 27, 2024
34f8fc1
wip: allow specifying a single file to lint
grunweg May 27, 2024
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 4 additions & 0 deletions .github/workflows/bors.yml
Original file line number Diff line number Diff line change
Expand Up @@ -166,6 +166,10 @@ jobs:
lean --version
lake --version

- name: run text-based style linters in Lean
run: |
lake exe lint_style

- name: build cache
run: |
lake build cache
Expand Down
4 changes: 4 additions & 0 deletions .github/workflows/build.yml
Original file line number Diff line number Diff line change
Expand Up @@ -173,6 +173,10 @@ jobs:
lean --version
lake --version

- name: run text-based style linters in Lean
run: |
lake exe lint_style

- name: build cache
run: |
lake build cache
Expand Down
4 changes: 4 additions & 0 deletions .github/workflows/build.yml.in
Original file line number Diff line number Diff line change
Expand Up @@ -152,6 +152,10 @@ jobs:
lean --version
lake --version

- name: run text-based style linters in Lean
run: |
lake exe lint_style

- name: build cache
run: |
lake build cache
Expand Down
4 changes: 4 additions & 0 deletions .github/workflows/build_fork.yml
Original file line number Diff line number Diff line change
Expand Up @@ -170,6 +170,10 @@ jobs:
lean --version
lake --version

- name: run text-based style linters in Lean
run: |
lake exe lint_style

- name: build cache
run: |
lake build cache
Expand Down
2 changes: 2 additions & 0 deletions Mathlib.lean
Original file line number Diff line number Diff line change
Expand Up @@ -3787,6 +3787,7 @@ import Mathlib.Tactic.Linter
import Mathlib.Tactic.Linter.AttributeInstanceIn
import Mathlib.Tactic.Linter.HashCommandLinter
import Mathlib.Tactic.Linter.Lint
import Mathlib.Tactic.Linter.TextBased
import Mathlib.Tactic.Measurability
import Mathlib.Tactic.Measurability.Init
import Mathlib.Tactic.MkIffOfInductiveProp
Expand Down Expand Up @@ -3860,6 +3861,7 @@ import Mathlib.Tactic.Simps.NotationClass
import Mathlib.Tactic.SlimCheck
import Mathlib.Tactic.SplitIfs
import Mathlib.Tactic.Spread
import Mathlib.Tactic.StyleLinters
import Mathlib.Tactic.Substs
import Mathlib.Tactic.SuccessIfFailWithMsg
import Mathlib.Tactic.SudoSetOption
Expand Down
3 changes: 2 additions & 1 deletion Mathlib/Data/QPF/Multivariate/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -72,7 +72,8 @@ each proves that some operations on functors preserves the QPF structure

## Reference

! * [Jeremy Avigad, Mario M. Carneiro and Simon Hudon, *Data Types as Quotients of Polynomial Functors*][avigad-carneiro-hudon2019]
* [Jeremy Avigad, Mario M. Carneiro and Simon Hudon,
*Data Types as Quotients of Polynomial Functors*][avigad-carneiro-hudon2019]
-/


Expand Down
2 changes: 2 additions & 0 deletions Mathlib/Tactic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -115,6 +115,7 @@ import Mathlib.Tactic.Linter
import Mathlib.Tactic.Linter.AttributeInstanceIn
import Mathlib.Tactic.Linter.HashCommandLinter
import Mathlib.Tactic.Linter.Lint
import Mathlib.Tactic.Linter.TextBased
import Mathlib.Tactic.Measurability
import Mathlib.Tactic.Measurability.Init
import Mathlib.Tactic.MkIffOfInductiveProp
Expand Down Expand Up @@ -188,6 +189,7 @@ import Mathlib.Tactic.Simps.NotationClass
import Mathlib.Tactic.SlimCheck
import Mathlib.Tactic.SplitIfs
import Mathlib.Tactic.Spread
import Mathlib.Tactic.StyleLinters
import Mathlib.Tactic.Substs
import Mathlib.Tactic.SuccessIfFailWithMsg
import Mathlib.Tactic.SudoSetOption
Expand Down
429 changes: 429 additions & 0 deletions Mathlib/Tactic/Linter/TextBased.lean

Large diffs are not rendered by default.

68 changes: 68 additions & 0 deletions Mathlib/Tactic/StyleLinters.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1,68 @@
/-
Copyright (c) 2024 Michael Rothgang. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Michael Rothgang
-/

import Lean.Elab.Command
import Lean.Linter.Util
import Batteries.Data.String.Basic

/-!
## Style linters

Linters which are purely about stylistic things: ported from the `lint-style.py` script.
-/

open Lean Elab Command

namespace Mathlib.Linter.Style.SetOption

/-- Whether a syntax element is a `set_option` call:
Return the name of the option being set, if any. -/
def parse_set_option : Syntax → Option (Ident)
-- This handles all four cases: string, number, true and false
| `(command|set_option $name:ident $_val) => some name
| `(set_option $name:ident $_val in $_x) => some name
| `(tactic|set_option $name:ident $_val in $_x) => some name
| _ => none

/-- Whether a given piece of syntax is a `set_option` command, tactic or term. -/
def is_set_option : Syntax → Bool :=
fun stx ↦ parse_set_option stx matches some _name

/-- The `setOption` linter emits a warning on a `set_option ...`. -/
register_option linter.setOption : Bool := {
defValue := true
descr := "enable the `setOption` linter"
}

/-- Gets the value of the `linter.setOption` option. -/
def getLinterHash (o : Options) : Bool := Linter.getLinterValue linter.setOption o

/-- The `setOption` linter: this lints any `set_option` command, term or tactic
which sets a `pp`, `profiler` or `trace` option.

**Why is this bad?** These options are good for debugging, but should not be
used in production code.
-/
def setOptionLinter : Linter where
run := withSetOptionIn fun stx => do
unless getLinterHash (← getOptions) do
return
if (← MonadState.get).messages.hasErrors then
return
match stx.findStack? (fun _ ↦ true) is_set_option with
| some ((head, _n)::_chain) =>
match parse_set_option head with
| some (name) =>
-- Drop a leading `
let name := (toString name).drop 1
if name.startsWith "pp." || name.startsWith "profiler." || name.startsWith "trace." then
Linter.logLint linter.setOption head m!"Forbidden set_option `{name}`; please remove"
| _ => return
| _ => return

initialize addLinter setOptionLinter

end Mathlib.Linter.Style.SetOption
8 changes: 8 additions & 0 deletions lakefile.lean
Original file line number Diff line number Diff line change
Expand Up @@ -61,6 +61,14 @@ lean_exe shake where
root := `Shake.Main
supportInterpreter := true

/-- `lake exe lint_style` runs text-based style lints. -/
lean_exe lint_style where
root := `Mathlib.Tactic.Linter.TextBased

/-- `lake exe update_style_exceptions` update the style exceptions file. -/
lean_exe update_style_exceptions where
srcDir := "scripts"

/--
`lake exe pole` queries the Mathlib speedcenter for build times for the current commit,
and then calculates the longest pole
Expand Down
Loading
Loading