nolints stats

Stream: general

[Johan Commelin]

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]

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]

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

[Johan Commelin]

I have not yet investigated

[Johan Commelin]

0fc45dcd16b7042179efb36a8e62f908bf0bd0e9:4086
32b32ad912406254ac7ddb7100d50f00b86e46f5:3210

[Johan Commelin]

https://github.com/leanprover-community/mathlib/commit/0fc45dcd16b7042179efb36a8e62f908bf0bd0e9
feat(tactic/lint): support @[nolint unused_arguments] (#2041)

[Rob Lewis]

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]

Still a nice graph!

[Johan Commelin]

Ok, let me try again (-;

[Johan Commelin]

I'll have lunch first

[Rob Lewis]

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]

Update:
nolints_stats.png

[Johan Commelin]

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]

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]

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

[Sebastien Gouezel]

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

[Johan Commelin]

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

[Johan Commelin]

I guess I should bookmark it...

[Bryan Gin-ge Chen]

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

[Johan Commelin]

@Bryan Gin-ge Chen Thanks!

[Johan Commelin]

This graph is not automatically updated, is it?

[Johan Commelin]

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

[Rob Lewis]

It is updated, yeah.

[Johan Commelin]

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]

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]

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]

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]

What exactly is this measuring?

[Kenny Lau]

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

[Johan Commelin]

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

[Johan Commelin]

Or sort -rn

[Kenny Lau]

but i like python