Unused variables

Stream: general

[Damiano Testa]

Prompted by a question of Bhavik (see #17178), I am trying to systematically find variables that are unused.

[Damiano Testa]

It turns out that there are really a lot! I suspect that quite a few are a consequence of splitting files and copying over variable commands where they are no longer needed.

[Damiano Testa]

#17261 is a first batch of removals.

[Damiano Testa]

The linter that found them is still not really ready for review, since it currently is incapable of dealing with defs, but has still flagged thousands of candidates for removal.

[Damiano Testa]

Is this something that is desirable?

[Michael Rothgang]

Can the same idea be adapted to find unused opens? That's something I wanted to think about for quite a while, but never got important enough...

[Damiano Testa]

Yes, a similar strategy can also be used for unused open: the inclusion mechanism is different, but the kind of tracking is very similar.

[Damiano Testa]

I have been making progress towards a linter that catches variables that can be removed. It is not yet complete, but it has already found a lot of simplifications (many of which are already merged).

[Damiano Testa]

However, the current version find over 4k exceptions in mathlib (unfortunately, some of these are false positives and the corresponding variables are used, but I have not managed to find a good way of excluding them from the linter).

[Damiano Testa]

Would it be desirable to produce a version of the linter that is conservative, may not flag every unused variable, but certainly flags unused ones, and do a mass substitution?

[Damiano Testa]

This would still likely imply thousands of changes to hundreds, if not thousands of files.

[Damiano Testa]

#17566 is the latest batch of removals, in case you are interested.

[Ruben Van de Velde]

If you feel up for it, I'd lean towards reviewable chunks, but it sounds like that could keep you busy for quite a while. Alternatively you could land the linter off by default and we could spread the work around a bit.

[Damiano Testa]

I'll PR a few more chunks for a while, at least until the linter is more reliable. I'll probably switch to distributing the effort, once the linter is more "independent", though.

[Damiano Testa]

#17574

[Damiano Testa]

#17579

[Damiano Testa]

I cleaned up a little the linter and opened #17715.

[Damiano Testa]

This is by no means a final version, but it is there in case someone feels like checking out the branch, removing some unused variables and leave mathlib in a better shape!