Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#4898)
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 Nov 4, 2020
1 parent 23a2767 commit 16e3871
Show file tree
Hide file tree
Showing 2 changed files with 39 additions and 46 deletions.
80 changes: 39 additions & 41 deletions scripts/copy-mod-doc-exceptions.txt
View file
Expand Up @@ -241,16 +241,16 @@ src/analysis/normed_space/inner_product.lean : line 352 : ERR_LIN : Line has mor
src/analysis/normed_space/inner_product.lean : line 811 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 830 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 892 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/multilinear.lean : line 1022 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/multilinear.lean : line 110 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/multilinear.lean : line 143 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/multilinear.lean : line 332 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/multilinear.lean : line 379 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/multilinear.lean : line 654 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/multilinear.lean : line 693 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/multilinear.lean : line 731 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/multilinear.lean : line 864 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/multilinear.lean : line 897 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/multilinear.lean : line 992 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/multilinear.lean : line 409 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/multilinear.lean : line 684 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/multilinear.lean : line 723 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/multilinear.lean : line 761 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/multilinear.lean : line 894 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/multilinear.lean : line 927 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/operator_norm.lean : line 163 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/operator_norm.lean : line 222 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/operator_norm.lean : line 34 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -406,19 +406,20 @@ src/category_theory/limits/functor_category.lean : line 115 : ERR_LIN : Line has
src/category_theory/limits/functor_category.lean : line 40 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/functor_category.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/category_theory/limits/lattice.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/category_theory/limits/limits.lean : line 1058 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 1081 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 1089 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 1110 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 1421 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 1426 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 1472 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 1506 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 1062 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 1085 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 1093 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 1114 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 1156 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 1419 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 1424 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 1470 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 1504 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 1523 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 1525 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 1527 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 1569 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 1613 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 1681 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 1567 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 1611 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 1679 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 233 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 425 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/limits.lean : line 578 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -524,7 +525,7 @@ src/category_theory/limits/shapes/zero.lean : line 124 : ERR_LIN : Line has more
src/category_theory/limits/shapes/zero.lean : line 271 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/shapes/zero.lean : line 67 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/types.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/category_theory/limits/types.lean : line 175 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/types.lean : line 179 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/types.lean : line 52 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/types.lean : line 57 : ERR_LIN : Line has more than 100 characters
src/category_theory/limits/types.lean : line 93 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -798,8 +799,8 @@ src/data/multiset/basic.lean : line 1720 : ERR_LIN : Line has more than 100 char
src/data/multiset/basic.lean : line 1729 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 1745 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 1748 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 1928 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 2052 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 1926 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 2050 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 542 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 666 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 677 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -1205,9 +1206,9 @@ src/linear_algebra/linear_independent.lean : line 886 : ERR_LIN : Line has more
src/linear_algebra/matrix.lean : line 622 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/matrix.lean : line 693 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/matrix.lean : line 706 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/matrix.lean : line 793 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/matrix.lean : line 847 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/multilinear.lean : line 107 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/multilinear.lean : line 443 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/multilinear.lean : line 460 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/multilinear.lean : line 63 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/multilinear.lean : line 78 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/special_linear_group.lean : line 53 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -1525,17 +1526,17 @@ src/tactic/converter/interactive.lean : line 53 : ERR_LIN : Line has more than 1
src/tactic/converter/old_conv.lean : line 272 : ERR_LIN : Line has more than 100 characters
src/tactic/converter/old_conv.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/tactic/core.lean : line 17 : ERR_MOD : Module docstring missing, or too late
src/tactic/core.lean : line 1789 : ERR_LIN : Line has more than 100 characters
src/tactic/core.lean : line 1877 : ERR_LIN : Line has more than 100 characters
src/tactic/core.lean : line 2072 : ERR_LIN : Line has more than 100 characters
src/tactic/core.lean : line 2135 : ERR_LIN : Line has more than 100 characters
src/tactic/core.lean : line 2143 : ERR_LIN : Line has more than 100 characters
src/tactic/core.lean : line 2167 : ERR_LIN : Line has more than 100 characters
src/tactic/core.lean : line 2168 : ERR_LIN : Line has more than 100 characters
src/tactic/core.lean : line 2194 : ERR_LIN : Line has more than 100 characters
src/tactic/core.lean : line 2287 : ERR_LIN : Line has more than 100 characters
src/tactic/core.lean : line 2291 : ERR_LIN : Line has more than 100 characters
src/tactic/core.lean : line 2292 : ERR_LIN : Line has more than 100 characters
src/tactic/core.lean : line 1792 : ERR_LIN : Line has more than 100 characters
src/tactic/core.lean : line 1880 : ERR_LIN : Line has more than 100 characters
src/tactic/core.lean : line 2075 : ERR_LIN : Line has more than 100 characters
src/tactic/core.lean : line 2138 : ERR_LIN : Line has more than 100 characters
src/tactic/core.lean : line 2146 : ERR_LIN : Line has more than 100 characters
src/tactic/core.lean : line 2170 : ERR_LIN : Line has more than 100 characters
src/tactic/core.lean : line 2171 : ERR_LIN : Line has more than 100 characters
src/tactic/core.lean : line 2197 : ERR_LIN : Line has more than 100 characters
src/tactic/core.lean : line 2290 : ERR_LIN : Line has more than 100 characters
src/tactic/core.lean : line 2294 : ERR_LIN : Line has more than 100 characters
src/tactic/core.lean : line 2295 : ERR_LIN : Line has more than 100 characters
src/tactic/core.lean : line 614 : ERR_LIN : Line has more than 100 characters
src/tactic/core.lean : line 629 : ERR_LIN : Line has more than 100 characters
src/tactic/core.lean : line 630 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -1577,10 +1578,10 @@ src/tactic/interactive_expr.lean : line 185 : ERR_LIN : Line has more than 100 c
src/tactic/interactive_expr.lean : line 186 : ERR_LIN : Line has more than 100 characters
src/tactic/interactive_expr.lean : line 232 : ERR_LIN : Line has more than 100 characters
src/tactic/interactive_expr.lean : line 242 : ERR_LIN : Line has more than 100 characters
src/tactic/interactive_expr.lean : line 363 : ERR_LIN : Line has more than 100 characters
src/tactic/interactive_expr.lean : line 408 : ERR_LIN : Line has more than 100 characters
src/tactic/interactive_expr.lean : line 434 : ERR_LIN : Line has more than 100 characters
src/tactic/interactive_expr.lean : line 368 : ERR_LIN : Line has more than 100 characters
src/tactic/interactive_expr.lean : line 413 : ERR_LIN : Line has more than 100 characters
src/tactic/interactive_expr.lean : line 439 : ERR_LIN : Line has more than 100 characters
src/tactic/interactive_expr.lean : line 444 : ERR_LIN : Line has more than 100 characters
src/tactic/interactive_expr.lean : line 76 : ERR_LIN : Line has more than 100 characters
src/tactic/interval_cases.lean : line 192 : ERR_LIN : Line has more than 100 characters
src/tactic/interval_cases.lean : line 230 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -1639,8 +1640,6 @@ src/tactic/local_cache.lean : line 193 : ERR_LIN : Line has more than 100 charac
src/tactic/local_cache.lean : line 219 : ERR_LIN : Line has more than 100 characters
src/tactic/local_cache.lean : line 29 : ERR_LIN : Line has more than 100 characters
src/tactic/local_cache.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/tactic/mk_iff_of_inductive_prop.lean : line 14 : ERR_MOD : Module docstring missing, or too late
src/tactic/mk_iff_of_inductive_prop.lean : line 167 : ERR_LIN : Line has more than 100 characters
src/tactic/monotonicity/basic.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/tactic/monotonicity/interactive.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/tactic/monotonicity/interactive.lean : line 191 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -1831,7 +1830,6 @@ src/topology/algebra/module.lean : line 554 : ERR_LIN : Line has more than 100 c
src/topology/algebra/module.lean : line 606 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/module.lean : line 673 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/multilinear.lean : line 185 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/multilinear.lean : line 298 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/multilinear.lean : line 46 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/multilinear.lean : line 60 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/open_subgroup.lean : line 10 : ERR_MOD : Module docstring missing, or too late
Expand Down
5 changes: 0 additions & 5 deletions scripts/nolints.txt
View file
Expand Up @@ -876,11 +876,6 @@ apply_nolint tactic.local_cache.internal.save_data doc_blame unused_arguments
-- tactic/localized.lean
apply_nolint localized_attr doc_blame

-- tactic/mk_iff_of_inductive_prop.lean
apply_nolint tactic.constr_to_prop doc_blame
apply_nolint tactic.mk_iff doc_blame
apply_nolint tactic.select doc_blame

-- tactic/monotonicity/basic.lean
apply_nolint tactic.interactive.compare doc_blame
apply_nolint tactic.interactive.filter_instances doc_blame
Expand Down

0 comments on commit 16e3871

Please sign in to comment.