diff --git a/scripts/nolints.txt b/scripts/nolints.txt index 6c79ed3d730df..97a37523b7f6e 100644 --- a/scripts/nolints.txt +++ b/scripts/nolints.txt @@ -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 diff --git a/scripts/style-exceptions.txt b/scripts/style-exceptions.txt index 1cb07a447aff5..bedcf1179fbb2 100644 --- a/scripts/style-exceptions.txt +++ b/scripts/style-exceptions.txt @@ -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 @@ -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 @@ -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