Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#6719)
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 Mar 17, 2021
1 parent b9ccb8f commit 3936f5f
Show file tree
Hide file tree
Showing 2 changed files with 9 additions and 16 deletions.
3 changes: 0 additions & 3 deletions scripts/nolints.txt
View file
Expand Up @@ -1132,9 +1132,6 @@ apply_nolint continuous_map.induced doc_blame
-- topology/maps.lean
apply_nolint inducing doc_blame

-- topology/metric_space/emetric_space.lean
apply_nolint has_edist doc_blame

-- topology/metric_space/gluing.lean
apply_nolint metric.glue_premetric doc_blame
apply_nolint metric.glue_space doc_blame
Expand Down
22 changes: 9 additions & 13 deletions scripts/style-exceptions.txt
View file
Expand Up @@ -32,7 +32,6 @@ src/category_theory/monad/basic.lean : line 9 : ERR_MOD : Module docstring missi
src/category_theory/monad/limits.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/category_theory/natural_transformation.lean : line 16 : ERR_MOD : Module docstring missing, or too late
src/category_theory/opposites.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/category_theory/products/associator.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/category_theory/products/basic.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/category_theory/products/bifunctor.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/category_theory/punit.lean : line 9 : ERR_MOD : Module docstring missing, or too late
Expand Down Expand Up @@ -164,7 +163,7 @@ src/data/seq/computation.lean : line 11 : ERR_MOD : Module docstring missing, or
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/set/basic.lean : line 2435 : ERR_LIN : Line has more than 100 characters
src/data/set/basic.lean : line 2439 : ERR_LIN : Line has more than 100 characters
src/data/set/basic.lean : line 897 : ERR_LIN : Line has more than 100 characters
src/data/set/disjointed.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/data/set/enumerate.lean : line 10 : ERR_MOD : Module docstring missing, or too late
Expand Down Expand Up @@ -215,9 +214,9 @@ src/geometry/manifold/local_invariant_properties.lean : line 211 : ERR_LIN : Lin
src/geometry/manifold/local_invariant_properties.lean : line 216 : ERR_LIN : Line has more than 100 characters
src/geometry/manifold/local_invariant_properties.lean : line 388 : ERR_LIN : Line has more than 100 characters
src/geometry/manifold/local_invariant_properties.lean : line 433 : ERR_LIN : Line has more than 100 characters
src/geometry/manifold/times_cont_mdiff.lean : line 1015 : ERR_LIN : Line has more than 100 characters
src/geometry/manifold/times_cont_mdiff.lean : line 1395 : ERR_LIN : Line has more than 100 characters
src/geometry/manifold/times_cont_mdiff.lean : line 1695 : ERR_LIN : Line has more than 100 characters
src/geometry/manifold/times_cont_mdiff.lean : line 1022 : ERR_LIN : Line has more than 100 characters
src/geometry/manifold/times_cont_mdiff.lean : line 1402 : ERR_LIN : Line has more than 100 characters
src/geometry/manifold/times_cont_mdiff.lean : line 1702 : ERR_LIN : Line has more than 100 characters
src/geometry/manifold/times_cont_mdiff.lean : line 244 : ERR_LIN : Line has more than 100 characters
src/geometry/manifold/times_cont_mdiff.lean : line 298 : ERR_LIN : Line has more than 100 characters
src/geometry/manifold/times_cont_mdiff.lean : line 355 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -555,18 +554,15 @@ src/topology/instances/real.lean : line 136 : ERR_LIN : Line has more than 100 c
src/topology/local_homeomorph.lean : line 567 : ERR_LIN : Line has more than 100 characters
src/topology/local_homeomorph.lean : line 578 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/basic.lean : line 17 : ERR_MOD : Module docstring missing, or too late
src/topology/metric_space/gromov_hausdorff.lean : line 61 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/isometry.lean : line 385 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/gromov_hausdorff.lean : line 62 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/premetric_space.lean : line 82 : ERR_LIN : Line has more than 100 characters
src/topology/omega_complete_partial_order.lean : line 85 : ERR_LIN : Line has more than 100 characters
src/topology/separation.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/topology/sheaves/forget.lean : line 147 : ERR_LIN : Line has more than 100 characters
src/topology/sheaves/presheaf.lean : line 106 : ERR_LIN : Line has more than 100 characters
src/topology/sheaves/presheaf.lean : line 108 : ERR_LIN : Line has more than 100 characters
src/topology/sheaves/presheaf.lean : line 40 : ERR_LIN : Line has more than 100 characters
src/topology/sheaves/presheaf.lean : line 57 : ERR_LIN : Line has more than 100 characters
src/topology/sheaves/presheaf.lean : line 58 : ERR_LIN : Line has more than 100 characters
src/topology/sheaves/presheaf.lean : line 94 : ERR_LIN : Line has more than 100 characters
src/topology/sheaves/presheaf.lean : line 97 : ERR_LIN : Line has more than 100 characters
src/topology/sheaves/presheaf.lean : line 96 : ERR_LIN : Line has more than 100 characters
src/topology/sheaves/presheaf.lean : line 99 : ERR_LIN : Line has more than 100 characters
src/topology/sheaves/presheaf_of_functions.lean : line 80 : ERR_LIN : Line has more than 100 characters
src/topology/sheaves/sheaf.lean : line 89 : ERR_LIN : Line has more than 100 characters
src/topology/sheaves/sheaf.lean : line 91 : ERR_LIN : Line has more than 100 characters
Expand All @@ -576,7 +572,7 @@ src/topology/sheaves/sheaf_of_functions.lean : line 168 : ERR_LIN : Line has mor
src/topology/sheaves/stalks.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/topology/sheaves/stalks.lean : line 128 : ERR_LIN : Line has more than 100 characters
src/topology/sheaves/stalks.lean : line 133 : ERR_LIN : Line has more than 100 characters
src/topology/subset_properties.lean : line 1097 : ERR_LIN : Line has more than 100 characters
src/topology/subset_properties.lean : line 1113 : ERR_LIN : Line has more than 100 characters
src/topology/tactic.lean : line 84 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/absolute_value.lean : line 71 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/compact_separated.lean : line 128 : ERR_LIN : Line has more than 100 characters
Expand Down

0 comments on commit 3936f5f

Please sign in to comment.