Syntax linting

Stream: general

[Damiano Testa]

The topic of maintaining style guidelines (and of an auto-formatter) frequently comes up. There is already a linter that tries to enforce that the pretty-printed syntax matches what has been typed. However, complying with it is not actually reasonable.

[Damiano Testa]

Still, for some parts of the code, I find that this linter could be useful. For instance, formatting the statement of a theorem (or maybe even just everything that comes before the :).

[Damiano Testa]

Would this be desirable?

[Damiano Testa]

(#general > Mathlib community meetings @ 💬 is the immediate previous discussion that triggered this thread.)

[Alex Meiburg]

The main place I see this failing would be anything involving casts, where typically the pretty-printed syntax doesn't even typecheck. Would there be some sort of special casing for that?

[Alex Meiburg]

Never mind, I see that someone had the same question in the linked thread. (For others coming here: casts are delaboration, not pretty-printing, so casts would be preserved in the same way as written.)

[Eric Wieser]

I think I've seen a round-tripping failure for Syntax -> String relating to overloaded [] notation, but I can't find the thread

[Damiano Testa]

Ok, I'll try to make it parse a small initial fragment of each declaration and I'll look at the output.

[Damiano Testa]

Even just pretty printing declarations up to := produces over 6k exceptions, we'll see how much extra special casing will be needed.