Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#9047)
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 Sep 7, 2021
1 parent 77f4ed4 commit c4f3707
Show file tree
Hide file tree
Showing 2 changed files with 1 addition and 75 deletions.
8 changes: 0 additions & 8 deletions scripts/nolints.txt
View file
Expand Up @@ -329,14 +329,6 @@ apply_nolint polynomial.eval_sub_factor doc_blame
apply_nolint polynomial.pow_add_expansion doc_blame
apply_nolint polynomial.pow_sub_pow_factor doc_blame

-- data/real/cau_seq_completion.lean
apply_nolint cau_seq.completion.Cauchy doc_blame
apply_nolint cau_seq.completion.field doc_blame
apply_nolint cau_seq.completion.mk doc_blame
apply_nolint cau_seq.completion.of_rat doc_blame
apply_nolint cau_seq.is_complete doc_blame
apply_nolint cau_seq.lim doc_blame

-- data/seq/computation.lean
apply_nolint computation.bind.F doc_blame
apply_nolint computation.bind.G doc_blame
Expand Down
68 changes: 1 addition & 67 deletions scripts/style-exceptions.txt
View file
Expand Up @@ -52,7 +52,7 @@ src/data/qpf/univariate/basic.lean : line 35 : ERR_LIN : Line has more than 100
src/data/seq/computation.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/data/seq/parallel.lean : line 14 : ERR_MOD : Module docstring missing, or too late
src/data/seq/seq.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/data/seq/wseq.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/data/seq/wseq.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/data/sigma/basic.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/deprecated/subfield.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/deprecated/subring.lean : line 10 : ERR_MOD : Module docstring missing, or too late
Expand All @@ -65,58 +65,21 @@ src/tactic/auto_cases.lean : line 8 : ERR_MOD : Module docstring missing, or too
src/tactic/chain.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/tactic/converter/binders.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/tactic/converter/interactive.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/tactic/converter/interactive.lean : line 53 : ERR_LIN : Line has more than 100 characters
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 2194 : ERR_LIN : Line has more than 100 characters
src/tactic/core.lean : line 2355 : ERR_LIN : Line has more than 100 characters
src/tactic/delta_instance.lean : line 67 : ERR_LIN : Line has more than 100 characters
src/tactic/delta_instance.lean : line 75 : ERR_LIN : Line has more than 100 characters
src/tactic/delta_instance.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/tactic/elide.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/tactic/ext.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/tactic/fin_cases.lean : line 121 : ERR_LIN : Line has more than 100 characters
src/tactic/fin_cases.lean : line 13 : ERR_MOD : Module docstring missing, or too late
src/tactic/find.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/tactic/generalizes.lean : line 117 : ERR_LIN : Line has more than 100 characters
src/tactic/hint.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/tactic/induction.lean : line 1329 : ERR_RNT : Reserved notation outside tactic.reserved_notation
src/tactic/interactive.lean : line 1063 : ERR_LIN : Line has more than 100 characters
src/tactic/interactive.lean : line 385 : ERR_LIN : Line has more than 100 characters
src/tactic/interactive.lean : line 649 : ERR_LIN : Line has more than 100 characters
src/tactic/interactive.lean : line 852 : ERR_LIN : Line has more than 100 characters
src/tactic/interactive.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/tactic/interactive_expr.lean : line 153 : ERR_LIN : Line has more than 100 characters
src/tactic/interactive_expr.lean : line 173 : ERR_LIN : Line has more than 100 characters
src/tactic/interactive_expr.lean : line 177 : ERR_LIN : Line has more than 100 characters
src/tactic/interactive_expr.lean : line 185 : ERR_LIN : Line has more than 100 characters
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 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 246 : ERR_LIN : Line has more than 100 characters
src/tactic/interval_cases.lean : line 32 : ERR_MOD : Module docstring missing, or too late
src/tactic/lean_core_docs.lean : line 733 : ERR_LIN : Line has more than 100 characters
src/tactic/lean_core_docs.lean : line 766 : ERR_LIN : Line has more than 100 characters
src/tactic/linarith/elimination.lean : line 121 : ERR_LIN : Line has more than 100 characters
src/tactic/linarith/parsing.lean : line 19 : ERR_LIN : Line has more than 100 characters
src/tactic/linarith/preprocessing.lean : line 228 : ERR_LIN : Line has more than 100 characters
src/tactic/linarith/preprocessing.lean : line 259 : ERR_LIN : Line has more than 100 characters
src/tactic/linarith/preprocessing.lean : line 260 : ERR_LIN : Line has more than 100 characters
src/tactic/linarith/preprocessing.lean : line 305 : ERR_LIN : Line has more than 100 characters
src/tactic/lint/default.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/tactic/local_cache.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/tactic/monotonicity/basic.lean : line 8 : 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
src/tactic/monotonicity/interactive.lean : line 467 : ERR_LIN : Line has more than 100 characters
src/tactic/monotonicity/interactive.lean : line 469 : ERR_LIN : Line has more than 100 characters
src/tactic/monotonicity/interactive.lean : line 490 : ERR_LIN : Line has more than 100 characters
src/tactic/monotonicity/lemmas.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/tactic/noncomm_ring.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/tactic/nth_rewrite/basic.lean : line 8 : ERR_MOD : Module docstring missing, or too late
Expand All @@ -142,51 +105,22 @@ src/tactic/omega/nat/sub_elim.lean : line 7 : ERR_MOD : Module docstring missing
src/tactic/omega/prove_unsats.lean : line 7 : ERR_MOD : Module docstring missing, or too late
src/tactic/omega/term.lean : line 7 : ERR_MOD : Module docstring missing, or too late
src/tactic/push_neg.lean : line 12 : ERR_MOD : Module docstring missing, or too late
src/tactic/push_neg.lean : line 188 : ERR_LIN : Line has more than 100 characters
src/tactic/push_neg.lean : line 189 : ERR_LIN : Line has more than 100 characters
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/show_term.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/tactic/simpa.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/tactic/slice.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/tactic/slim_check.lean : line 186 : ERR_LIN : Line has more than 100 characters
src/tactic/slim_check.lean : line 188 : ERR_LIN : Line has more than 100 characters
src/tactic/slim_check.lean : line 189 : ERR_LIN : Line has more than 100 characters
src/tactic/slim_check.lean : line 196 : ERR_LIN : Line has more than 100 characters
src/tactic/slim_check.lean : line 197 : ERR_LIN : Line has more than 100 characters
src/tactic/slim_check.lean : line 198 : ERR_LIN : Line has more than 100 characters
src/tactic/slim_check.lean : line 199 : ERR_LIN : Line has more than 100 characters
src/tactic/slim_check.lean : line 203 : ERR_LIN : Line has more than 100 characters
src/tactic/slim_check.lean : line 205 : ERR_LIN : Line has more than 100 characters
src/tactic/solve_by_elim.lean : line 161 : ERR_LIN : Line has more than 100 characters
src/tactic/solve_by_elim.lean : line 175 : ERR_LIN : Line has more than 100 characters
src/tactic/solve_by_elim.lean : line 99 : ERR_LIN : Line has more than 100 characters
src/tactic/split_ifs.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/tactic/split_ifs.lean : line 56 : ERR_LIN : Line has more than 100 characters
src/tactic/squeeze.lean : line 215 : ERR_LIN : Line has more than 100 characters
src/tactic/squeeze.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/tactic/subtype_instance.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/tactic/tauto.lean : line 35 : ERR_LIN : Line has more than 100 characters
src/tactic/tauto.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/tactic/tfae.lean : line 13 : ERR_MOD : Module docstring missing, or too late
src/tactic/tidy.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/tactic/tidy.lean : line 43 : ERR_LIN : Line has more than 100 characters
src/tactic/transfer.lean : line 101 : ERR_LIN : Line has more than 100 characters
src/tactic/transfer.lean : line 111 : ERR_LIN : Line has more than 100 characters
src/tactic/transfer.lean : line 112 : ERR_LIN : Line has more than 100 characters
src/tactic/transfer.lean : line 113 : ERR_LIN : Line has more than 100 characters
src/tactic/transfer.lean : line 6 : ERR_MOD : Module docstring missing, or too late
src/tactic/transform_decl.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/tactic/transform_decl.lean : line 98 : ERR_LIN : Line has more than 100 characters
src/tactic/transport.lean : line 45 : ERR_LIN : Line has more than 100 characters
src/tactic/trunc_cases.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/tactic/wlog.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/tactic/wlog.lean : line 181 : ERR_LIN : Line has more than 100 characters
src/tactic/wlog.lean : line 198 : ERR_LIN : Line has more than 100 characters
src/tactic/wlog.lean : line 218 : ERR_LIN : Line has more than 100 characters
src/tactic/wlog.lean : line 95 : ERR_LIN : Line has more than 100 characters
src/tactic/wlog.lean : line 97 : ERR_LIN : Line has more than 100 characters
src/testing/slim_check/gen.lean : line 133 : ERR_LIN : Line has more than 100 characters
src/testing/slim_check/gen.lean : line 144 : ERR_LIN : Line has more than 100 characters
src/testing/slim_check/gen.lean : line 83 : ERR_LIN : Line has more than 100 characters
Expand Down

0 comments on commit c4f3707

Please sign in to comment.