Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#5730)
Browse files Browse the repository at this point in the history 
I am happy to remove some nolints for you!
  • Loading branch information
@leanprover-community-bot
leanprover-community-bot committed Jan 14, 2021
1 parent 71a3261 commit c050452
Show file tree
Hide file tree
Showing 2 changed files with 5 additions and 17 deletions.
3 changes: 0 additions & 3 deletions scripts/nolints.txt
View file
Expand Up @@ -825,9 +825,6 @@ apply_nolint auto.preprocess_goal doc_blame
apply_nolint auto.whnf_reducible doc_blame
apply_nolint tactic.interactive.revert_all doc_blame

-- tactic/generalize_proofs.lean
apply_nolint tactic.generalize_proofs doc_blame

-- tactic/interactive.lean
apply_nolint tactic.interactive.collect_struct doc_blame
apply_nolint tactic.interactive.collect_struct' doc_blame
Expand Down
19 changes: 5 additions & 14 deletions scripts/style-exceptions.txt
View file
Expand Up @@ -223,7 +223,7 @@ src/analysis/normed_space/operator_norm.lean : line 34 : ERR_LIN : Line has more
src/analysis/normed_space/operator_norm.lean : line 645 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/operator_norm.lean : line 91 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/arsinh.lean : line 7 : ERR_MOD : Module docstring missing, or too late
src/analysis/special_functions/pow.lean : line 1357 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/pow.lean : line 1390 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/pow.lean : line 295 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/pow.lean : line 296 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/pow.lean : line 548 : ERR_LIN : Line has more than 100 characters
Expand All @@ -240,8 +240,7 @@ src/analysis/special_functions/trigonometric.lean : line 1476 : ERR_LIN : Line h
src/analysis/special_functions/trigonometric.lean : line 2037 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 2087 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 2159 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 2343 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 2849 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 2845 : ERR_LIN : Line has more than 100 characters
src/analysis/specific_limits.lean : line 84 : ERR_LIN : Line has more than 100 characters
src/category_theory/abelian/exact.lean : line 70 : ERR_LIN : Line has more than 100 characters
src/category_theory/abelian/exact.lean : line 76 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -516,12 +515,6 @@ src/category_theory/whiskering.lean : line 31 : ERR_LIN : Line has more than 100
src/category_theory/whiskering.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/combinatorics/pigeonhole.lean : line 87 : ERR_LIN : Line has more than 100 characters
src/computability/partrec_code.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/computability/reduce.lean : line 168 : ERR_LIN : Line has more than 100 characters
src/computability/reduce.lean : line 270 : ERR_LIN : Line has more than 100 characters
src/computability/reduce.lean : line 52 : ERR_LIN : Line has more than 100 characters
src/computability/reduce.lean : line 55 : ERR_LIN : Line has more than 100 characters
src/computability/reduce.lean : line 87 : ERR_LIN : Line has more than 100 characters
src/computability/reduce.lean : line 94 : ERR_LIN : Line has more than 100 characters
src/computability/tm_computable.lean : line 110 : ERR_LIN : Line has more than 100 characters
src/computability/tm_computable.lean : line 124 : ERR_LIN : Line has more than 100 characters
src/computability/tm_computable.lean : line 129 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -747,8 +740,8 @@ src/data/mv_polynomial/variables.lean : line 34 : ERR_LIN : Line has more than 1
src/data/mv_polynomial/variables.lean : line 621 : ERR_LIN : Line has more than 100 characters
src/data/nat/basic.lean : line 109 : ERR_LIN : Line has more than 100 characters
src/data/nat/basic.lean : line 870 : ERR_LIN : Line has more than 100 characters
src/data/nat/cast.lean : line 101 : ERR_LIN : Line has more than 100 characters
src/data/nat/cast.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/data/nat/cast.lean : line 118 : ERR_LIN : Line has more than 100 characters
src/data/nat/dist.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/data/nat/enat.lean : line 373 : ERR_LIN : Line has more than 100 characters
src/data/nat/gcd.lean : line 185 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -1420,7 +1413,6 @@ src/tactic/find_unused.lean : line 44 : ERR_LIN : Line has more than 100 charact
src/tactic/finish.lean : line 338 : ERR_LIN : Line has more than 100 characters
src/tactic/finish.lean : line 425 : ERR_LIN : Line has more than 100 characters
src/tactic/finish.lean : line 485 : ERR_LIN : Line has more than 100 characters
src/tactic/generalize_proofs.lean : line 7 : ERR_MOD : Module docstring missing, or too late
src/tactic/generalizes.lean : line 118 : ERR_LIN : Line has more than 100 characters
src/tactic/group.lean : line 36 : ERR_LIN : Line has more than 100 characters
src/tactic/hint.lean : line 57 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -1541,9 +1533,8 @@ src/tactic/push_neg.lean : line 184 : ERR_LIN : Line has more than 100 character
src/tactic/restate_axiom.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/tactic/rewrite.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/tactic/rewrite_all/basic.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/tactic/ring.lean : line 515 : ERR_LIN : Line has more than 100 characters
src/tactic/ring.lean : line 546 : ERR_LIN : Line has more than 100 characters
src/tactic/ring.lean : line 618 : ERR_LIN : Line has more than 100 characters
src/tactic/ring.lean : line 521 : ERR_LIN : Line has more than 100 characters
src/tactic/ring.lean : line 626 : ERR_LIN : Line has more than 100 characters
src/tactic/ring2.lean : line 482 : ERR_LIN : Line has more than 100 characters
src/tactic/ring_exp.lean : line 1549 : ERR_LIN : Line has more than 100 characters
src/tactic/show_term.lean : line 8 : ERR_MOD : Module docstring missing, or too late
Expand Down

0 comments on commit c050452

Please sign in to comment.