MultiGoal linter

Stream: mathlib4

[Damiano Testa]

This is the announcement of a new linter acting on Mathlib: the multiGoal linter.

The linter will flag missing focusing dots (·, typed \.). It highlights the lines that should be indented (the first should have an · added, the remaining just -- 2 spaces), until it reaches either the end of the proof, or a tactic that "stops" the linter.

[Damiano Testa]

As usual, bug reports and usability issues are welcome!

[Joachim Breitner]

Very nice! Hopefully after maturing in mathlib this can become standard for lean.

A future step is maybe that at the end of a tactic line at the end of a block, there is a tab-able completion that adds the right amount of bullets (or case tactics), so that one immediately sees the effect of the current tactic, and doesn't have to write the bullets manually. Of course that's easier said than done, with dependent sub goals that will disappear after solving others etc.

[Henrik Böving]

I got two questions regarding this:

1. It appears you have a couple of unextensible whitelists in the linter. That means everyone downstream of mathlib can now only work with these whitelists and nobody can flag their own tactics as whitelisted anymore. I feel like making these whitelists extensible, e.g. through some attribute, would make sense to fix this.
2. Is this one of the linters that run live in the editor or is this only executed in CI? If it runs live in the editor, have you benchmarked this at all? Going over every info tree node sounds like a good recipe for slowdown in big proofs.

[Damiano Testa]

Joachim Breitner said:

Very nice! Hopefully after maturing in mathlib this can become standard for lean.

A future step is maybe that at the end of a tactic line at the end of a block, there is a tab-able completion that adds the right amount of bullets (or case tactics), so that one immediately sees the effect of the current tactic, and doesn't have to write the bullets manually. Of course that's easier said than done, with dependent sub goals that will disappear after solving others etc.

I had thought of an post-completion code-action that would add the relevant indentations/·, but having an "auto-structuring" would also be nice! I agree that it is somewhat tricky with disappearing goals, but I found that those were relatively rare. Anyway, I'll keep this in mind!

[Damiano Testa]

Henrik Böving said:

I got two questions regarding this:

1. It appears you have a couple of unextensible whitelists in the linter. That means everyone downstream of mathlib can now only work with these whitelists and nobody can flag their own tactics as whitelisted anymore. I feel like making these whitelists extensible, e.g. through some attribute, would make sense to fix this.

That is a good point, although for the moment the linter is off by default outside of mathlib. I agree that it is sub-optimal that you have to live with the given exemptions, so I'll look into extensibility, although I would first wait to see how it works as is: adding new tactics to mathlib is pretty rare, so I'll wait a bit for that.

Henrik Böving said:

2. Is this one of the linters that run live in the editor or is this only executed in CI? If it runs live in the editor, have you benchmarked this at all? Going over every info tree node sounds like a good recipe for slowdown in big proofs.

The linter actually runs live in the editor as well. I find it very hard to know what can be slow, but I would like to learn: if you have the patience to give me some guidance, I am happy to use this linter as an excuse to learn!

[Damiano Testa]

(Also, my experience "fixing" the linter warnings did not make it appear visibly slow, but that is a very subjective measure. Note also that the linter only looks at completed proofs, not partial ones -- that probably mitigates its slow-down.)

[Damiano Testa]

Henrik, I'm thinking about ways to speed up the linter. Before I start to write some code, do you think it that it is worthwhile to scan the command syntax looking for "tactic" nodes, recording their positions and then recursing into the infotree, but only acting when the position of the node is one of the "tactic" ones?