Small Linting of the code base to have a tab of 2

[thomas-lamiaux]

I was tired of non-uniform indentation of the stdlib, so I used Python 3 and Claude to write a very basic linter:

• The Content of modules, sections, proofs and obligations have an indent of 2 except one line proofs
• The content inside each block was not modified but only indented so if it was not properly indented it still is
• It does nothing more

Since it is a bit simplistic, the result is not perfect but it looks much better to me and easier to navigate than it used to be.
Tell me if you are interested of merging. If you are interested I am also joining the script
linter_MSP.py

Note there are a lot of diff dues the extensive use Section in the code base, even when not needed apparently for documentation purpose. For Rocq in general, I believe it would be great to have a linter, e.g. integrated with vsrocq but I don't know how 😅

[andres-erbsen]

I think having an auto-formatted style would be nice. Details may take quite a bit of figuring out, though.

Things that seem clearly right to me:

• the default indentation step is two spaces
  • if a line preceding an indentation step is wrapped, the wrapped part should be indented doubly
• bodies of module functors should be indented
• bodies of proofs and braced subproofs (if-multi-line) should be indented
• single-character bullets count as their own indentation, with following lines under the same bullet indented

Some clear suggestions:

• in proofs, content braced blocks should be indented even if the brace is not first on a line (here)

However, the following cases seem less clear to me:

• Should the body of a module that is just a namespace be indented? Even if it captures all definitions in the file? If only the idea to have separate command for namespaces was actually implemented...
• Should a section immediately inside a module be indented? If only we had a command that starts a module and a section right away...
• Based on similar reasoning, should a section that contains all definitions in a file be indented?
• Should sections be indented at all?
• How should multi-character bullets be indented?

And there are many more ideas in Lean here

There's also implementation questions:

• How do we make sure this script does not break in the future, say with additions to the language?
• How to we make sure the commit that applies this change does not show up in git blame by default?
• Should the tool live in stdlib? (If stdlib was still in rocq, i'd say obviously yes, but now idk, maybe it should go there...)

[thomas-lamiaux]

This is a very small attempted and I don't understand the script fully nor it is the point, it was more of a oneshoot attempted to get sth better because right now it is painful

On the indenting rules

Should the body of a module that is just a namespace be indented?

Yes

Even if it captures all definitions in the file?

What is the point then, just do Require rather than Require Import

Should a section immediately inside a module be indented?

I believe so, except if it captures all the definitions in the module ?

Should sections be indented at all?

Most definitely to know what variables are available when, if your section has no variable, then there should not be a section, it is not meant for documenting

Indenting all sections is not perfect but it is good enough result to me

[andres-erbsen]

Hmm, I'm not sure how appealing a oneshot is. Auto-formatting is obviously desirable because it gives a quick out to all arguments about formatting, but I don't think just converting to the proposed style once would have the same effect, and then what's the point? And just looking at some more changes, what the script did in Streams.v:19 and ZmodDef.v:8 looks questionable to me already in a way separate from the conceptual questions. I'd rather just decide that anything goes on formatting, no nitpicking, but I realize that it may be challenging to get other devs to meaningfully agree to that.

Even if it captures all definitions in the file?
What is the point then, just do Require rather than Require Import

The point is namespacing. For example, there are a bunch of files with module Z, ZArith exports all of them, users write Z.blah without knowing what file it's from. I'm not sure it's ideal, but it's an important enough use case that a namespacing feature was proposed for it in Rocq (and implemented in Lean). (In Z it's with module functors sometimes, which makes the question moot, Zmod follows the same pattern without functors.)

if your section has no variable, then there should not be a section, it is not meant for documenting

It sure is used this way in btauto and Vector for example. Maybe it shouldn't be, but just changing existing indentation doesn't feel like a strong enough precedent to enforce that.

[thomas-lamiaux]

Hmm, I'm not sure how appealing a oneshot is. [...] I don't think just converting to the proposed style once would have the same effect, and then what's the point?

Basically, if you have a uniform style, even in the absence of autoformatting, it is much easier to check that new PR respect it and in the meantine the repo is already much better

And just looking at some more changes, what the script did in Streams.v:19 and ZmodDef.v:8 looks questionable to me already in a way separate from the conceptual questions.

Possible, I have checked many files but not all, as mentioned it is an experiment hence while it is a draft PR.
It is not necessarily meant to be merged, but at least we'll have a trace if someone is interested.
Note, for module or sections, it should not be too hard to check if it is a name space or not, and have sth more custom.
Note also that due to Rocq complex parsing, I doubt it is possible to have a perfect solution either, but we can probably do sth good enough, if someone spend a bit of time on it.