Reject Rocq commands without locality specifiers

[pgiarrusso-sl]

Commands like Open Scope, Hint Resolve, Arguments etc should always come with locality specifiers.

Relying on defaults is error-prone and often causes bugs.

• the defaults are sometimes broken — they're hard to remember
• even when the defaults are sensible, they're often not what reviewers expect. We almost always want #[global] or #[export],
  but Rocq often chooses #[local], which effectively means the attribute is silently ignored.
• the inferred locality depends on whether we're in a section/module or not, which is often not apparent locally. (Usually the code is indented iff we're not at the top-level, but that's not reliable either).

Note: This is probably not actionable in isolation, but I'd want this to be part of a code linter that runs in CI. We had something at BlueRock. In addition, linting might be also useful for users or to train agents.

[pgiarrusso-sl]

cc @jhaag-skylabs-ai

[gmalecha-at-skylabs]

@pgiarrusso-sl What did we have at BlueRock for this? It would be easy to write a regular expression that finds this problem after the fact. I don't know how to enforce this in Rocq without a patch though. That said, we could potentially write that patch without too much difficulty.

[pgiarrusso-sl]

We had some Rocq linter from Jasper in CI — that we might to restore. I don't think we had this rule.
A fragile regexp might be easy, but a linter and a CI pipeline will have some framework for error reporting.

[jhaag-skylabs-ai]

@simon-skylabs mentioned has mentioned a "linter" to me/Lennart a few times. I'm not sure if it's the python one I wrote back at BR, or if it's something new that he's created.

---

The doc manager could be useful for scripting these edits -- although sed might be easier/quicker.

[gmalecha-at-skylabs]

The sentence splitter is probably enough, but doing it through the doc manager is probably easier.

I'm a bit torn between python and ocaml for this sort of thing though.

• The benefit of python is that it is much easier to extend with custom rules (which would be useful for things like brick or automation-specific code).
• The benefit of ocaml is that it might get more adoption from the community. The downside is that interesting extensions would require re-compilation so you'd have to think of it as a library that allows you to write custom rules.

The other option is to add these directly to the Rocq source tree which takes longer, but would have much greater visibility.

[simon-skylabs]

Do you think we could split the difference and use OCaml and put the rules in a config file on the side?

[pgiarrusso-sl]

I'm tempted to first focus on adding more rules first in the short/medium term — probably in Python.

Longer-term, what would the language for linting rules be?
I'm sure linting rules are metaprograms from Rocq files to warning lists — but should they be regexps on sources, on lexer outputs, OCaml functions on ASTs, ...? Will we have some linting rules that won't be expressible in some formats? Will we want any global analysis? Using OCaml ASTs would mean code would break on internal ASTs changes...

[gmalecha-at-skylabs]

Do you think we could split the difference and use OCaml and put the rules in a config file on the side?

TL;DR: I think we can code some features directly and then enable or disable them with a configuration file. I think more complex rules would need a programming language. The question is: "how far can you go with the simple stuff before you run out of steam?" I would prefer to not invent a new programming language for these, so reusing Python or Ocaml seem to be the obvious choices.

[rlepigre-skylabs-ai]

For this particular use-case, it might better to make this a warning in Rocq itself, and to configure it as an error in our workspace.

[pgiarrusso-sl]

My only concern is "would upstream merge the warning we want", but otherwise sure.

[rlepigre-skylabs-ai]

Let's see: #Rocq devs & plugin devs > Warn when no locality is specified on certain commands.

[gmalecha-at-skylabs]

It seems like (for this feature), the right thing is to make a PR to Rocq.