Reify the style-guide as a 'linter'?

[jamesmckinna]

After 10+ years (!?), the library style-guide has (slowly!) evolved, often lagging behind actual practice-on-the-ground in specific modules/hierarchies, to the point where we have quite detailed low-level 'design' decisions baked into the guide, and hopefully, therefore, also into subsequent contributed PRs.

But the key here is 'hopefully', because we neither have, nor offer, machine-support in the form of 'lint' for such guidelines.

Could we imagine having such a thing, and incorporating it into our CI workflow? Could we (collectively) live with the consequences? Do we want to?

[jamesmckinna]

Thanks for the endorsement... but I think I'm not the person to write such a thing! Offers welcome... ;-) I raised the issue after having an illuminating discussion with a former Google engineer about their processes and practices eg PR development and code review wrt 'house culture/style', and the observation that passing a linter is an important step which takes some of the heat/effort out before anyone invests time in code review...

... but of course my fear is that attempting to reify our policies in code would oblige us to be much more detailed in our prescriptions... so experience from other quarters welcome!

[gallais]

I 💯 agree that we should not leave mechanically-enforceable conventions
to Humans, who surely have better things to do.

However, I don't know of any such tool for Agda so this should probably be
an upstream feature request (at least for an everything-preserving parser
rather than the one we currently have that throws comments & whitespace
away)?

[JacquesCarette]

I've been thinking that I might set one of my summer students (I've got two coming) on infrastructure stuff. This could definitely fit into that. Though having to deal with the parser first makes it a little bit more daunting!

[jamesmckinna]

I've been thinking that I might set one of my summer students (I've got two coming) on infrastructure stuff. This could definitely fit into that. Though having to deal with the parser first makes it a little bit more daunting!

Thanks Jacques. I think that there are other admin/infrastructure things which make more immediate improvement, such as optimising our CI workflow #2248 (so that eg certain phases, eg HTML generation, running golden tests, ... don't fire on every push).