# Zulip Chat Archive

## Stream: general

### Topic: nolints stats

#### Johan Commelin (Apr 07 2020 at 10:12):

I thought it might be nice to see how the nolints file grows/shrinks over time. Here is a plot that starts with the first commit that `scripts/nolints.txt`

existed, and walks through every commit until todays `master`

.

nolints_stats.png

#### Johan Commelin (Apr 07 2020 at 10:13):

Script (generates the data in reverse chronological order):

#!/bin/bash while [ -f scripts/nolints.txt ] do echo "$(git rev-parse HEAD):$(wc -l scripts/nolints.txt)" >> nolint_stats.txt git checkout HEAD^ done

#### Patrick Massot (Apr 07 2020 at 10:14):

What is the new linter that caused the huge jump up?

#### Johan Commelin (Apr 07 2020 at 10:14):

I have not yet investigated

#### Johan Commelin (Apr 07 2020 at 10:15):

0fc45dcd16b7042179efb36a8e62f908bf0bd0e9:4086 32b32ad912406254ac7ddb7100d50f00b86e46f5:3210

#### Johan Commelin (Apr 07 2020 at 10:16):

https://github.com/leanprover-community/mathlib/commit/0fc45dcd16b7042179efb36a8e62f908bf0bd0e9

feat(tactic/lint): support @[nolint unused_arguments] (#2041)

#### Rob Lewis (Apr 07 2020 at 10:26):

Yeah, the big jump was just a restructuring of the file to have headers and whitespace. A slightly better measure would be number of non-whitespace, non-comment lines.

#### Rob Lewis (Apr 07 2020 at 10:27):

Still a nice graph!

#### Johan Commelin (Apr 07 2020 at 10:27):

Ok, let me try again (-;

#### Johan Commelin (Apr 07 2020 at 10:30):

I'll have lunch first

#### Rob Lewis (Apr 07 2020 at 10:31):

You can also get a sense of the change from leanprover-community-bot's commits. It's removed 345 lines since Feb 14.

#### Johan Commelin (Apr 07 2020 at 11:12):

Update:

nolints_stats.png

#### Johan Commelin (Apr 07 2020 at 11:14):

Script:

#!/bin/bash git checkout -q master while [ -f scripts/nolints.txt ] do echo "$(git rev-parse HEAD):$(grep . scripts/nolints.txt | grep -v '^--' | wc -l)" git checkout -q HEAD^ done | tac | sed 's/ script.*//' git checkout -q master

#### Johan Commelin (Apr 07 2020 at 11:15):

Then I ran `cut -f2 -d:`

on the output of that script, and saved it in `rev_stats.txt`

.

Finally, the following gnuplot script made the graph:

#!/usr/bin/gnuplot -persist set title "Lines in scripts/nolints.txt" set xlabel "git commit" set ylabel "#lines" plot "rev_stats.txt" u (column(0)):1:xtic(1) w l title ""

#### Rob Lewis (Apr 07 2020 at 11:16):

Nice. This is one curve we don't want to flatten.

#### Sebastien Gouezel (Apr 08 2020 at 19:08):

#2352 has been merged. 37 lines less in `nolints.txt`

.

#### Johan Commelin (Jun 09 2020 at 20:00):

I can no longer find the autogenerated graph of nolints statistics on the website...

#### Johan Commelin (Jun 09 2020 at 20:00):

I guess I should bookmark it...

#### Bryan Gin-ge Chen (Jun 09 2020 at 20:09):

Took me a sec to find it too: https://leanprover-community.github.io/mathlib_stats/nolints.png

#### Johan Commelin (Jun 09 2020 at 20:43):

@Bryan Gin-ge Chen Thanks!

#### Johan Commelin (Jul 06 2020 at 08:36):

This graph is not automatically updated, is it?

#### Johan Commelin (Jul 06 2020 at 08:39):

Or maybe it is, but Zulip is also updating the image in Bryan's post.

#### Rob Lewis (Jul 06 2020 at 10:02):

It is updated, yeah.

#### Johan Commelin (Jul 06 2020 at 13:24):

```
mathlib/scripts$ cat nolints_summary.sh
#!/bin/bash
input=nolints.txt
fn=''
cnt=0
while read -r line
do
case "$line" in
'-- '*)
cnt=0
fn=${line:3}
;;
apply*)
cnt=$(($cnt+1))
;;
'')
if [ $cnt -gt 0 ]
then
echo "$cnt $fn"
fi
;;
esac
done < "$input"
echo $(($cnt+1)) $fn
```

#### Johan Commelin (Jul 06 2020 at 13:25):

```
mathlib/scripts$ ./nolints_summary.sh | sort -n | tail -30
15 tactic/explode.lean
16 deprecated/subgroup.lean
16 tactic/monotonicity/basic.lean
17 data/fintype/basic.lean
17 data/matrix/basic.lean
17 group_theory/perm/sign.lean
17 tactic/converter/interactive.lean
19 data/list/defs.lean
19 linear_algebra/tensor_product.lean
21 control/monad/cont.lean
21 tactic/converter/binders.lean
21 tactic/interactive.lean
21 tactic/rewrite.lean
22 data/pnat/xgcd.lean
22 group_theory/coset.lean
23 category_theory/equivalence.lean
23 control/traversable/derive.lean
23 meta/coinductive_predicates.lean
25 control/fold.lean
25 set_theory/ordinal.lean
26 tactic/local_cache.lean
27 data/mllist.lean
28 data/fp/basic.lean
29 category_theory/limits/cones.lean
29 tactic/abel.lean
33 tactic/rcases.lean
38 tactic/converter/old_conv.lean
42 data/num/bitwise.lean
53 tactic/monotonicity/interactive.lean
64 data/num/basic.lean
```

#### Kenny Lau (Jul 07 2020 at 14:40):

```
import io
f = io.open("../scripts/nolints.txt","r",encoding="utf-8")
name = ""
freq = []
for line in f:
if line[0] == "-":
name = line[3:-6]
freq.append((0, name))
elif freq:
(count, name) = freq[-1]
freq[-1] = (count+1, name)
freq.sort()
for count, name in freq:
if count > 2: break
print(name, count-1)
```

#### Kenny Lau (Jul 07 2020 at 14:41):

```
algebra/group/defs 1
algebraic_geometry/prime_spectrum 1
control/traversable/lemmas 1
data/W 1
data/buffer/basic 1
data/dlist/basic 1
data/dlist/instances 1
data/fin 1
data/hash_map 1
data/int/modeq 1
data/int/parity 1
data/list/range 1
data/list/tfae 1
data/multiset/functor 1
data/multiset/pi 1
data/nat/enat 1
data/nat/prime 1
data/nat/sqrt 1
data/nat/totient 1
data/padics/padic_norm 1
data/quot 1
data/real/ereal 1
data/real/nnreal 1
data/set/enumerate 1
data/string/basic 1
field_theory/subfield 1
group_theory/presented_group 1
group_theory/sylow 1
logic/unique 1
measure_theory/category/Meas 1
measure_theory/measurable_space 1
measure_theory/measure_space 1
order/bounded_lattice 1
order/galois_connection 1
order/lexicographic 1
ring_theory/integral_closure 1
ring_theory/maps 1
ring_theory/multiplicity 1
ring_theory/subring 1
set_theory/cofinality 1
tactic/core 1
tactic/generalize_proofs 1
tactic/localized 1
tactic/monotonicity/lemmas 1
tactic/norm_num 1
tactic/omega/int/form 1
tactic/omega/nat/form 1
tactic/omega/nat/neg_elim 1
tactic/scc 1
tactic/subtype_instance 1
tactic/wlog 1
topology/algebra/ring 1
topology/algebra/uniform_ring 1
topology/category/TopCommRing 1
topology/homeomorph 1
topology/metric_space/isometry 1
topology/metric_space/premetric_space 1
topology/opens 1
topology/sheaves/stalks 1
topology/uniform_space/uniform_embedding 1
```

#### Johan Commelin (Jul 07 2020 at 14:43):

What exactly is this measuring?

#### Kenny Lau (Jul 07 2020 at 14:50):

instead of showing the hardest goals I've decided to show the easiest goals

#### Johan Commelin (Jul 07 2020 at 14:52):

Ooh, you could have taken my script and piped it through `tac`

#### Johan Commelin (Jul 07 2020 at 14:52):

Or `sort -rn`

#### Kenny Lau (Jul 07 2020 at 14:52):

but i like python

Last updated: Dec 20 2023 at 11:08 UTC