Coding Style: use of spaces
It seems we have a bit of a coding style mess in Prosa master
. I wrote a little script to check our usage of spaces before and after colons. It probably doesn't catch everything, but the output already shows that we have a fair bit of diversity in style:
Coding Style in Prosa (without classic Prosa)
Spacing after Lemma/Fact/Theorem/Hypothesis/Corollary name:
- 731 instances of no space before colon (good)
- 406 instances of a space before colon (bad)
Naming of hypotheses:
- 607 Hypothesis names start with 'H_' (good)
- 6 Hypothesis names do not start with 'H_' (bad)
Spacing in Variable/Variables/Context declaration:
- 550 instances of a space before colon (good)
- 183 instances of no space before colon (bad)
- 435 no colon at all (implicit Context)
Spacing in Definition/Fixpoint:
- 116 instances of a space before colon (good)
- 22 instances of no space before colon (bad)
- 123 no colon at all (no parameters)
Consistent spacing may seem like a minor thing, but it's quite annoying to some (e.g., me) and it's difficult to tell new contributors "just follow the style of existing code" if that code is all over the place.
So this issue serves to find consensus on this. If I recall correctly, at some point we agreed on the following:
-
Variable foo : ItsType.
— space before and after colon when giving types of variables or parameters. -
Context {SomeConcept : ItsType}.
— as above. -
Hypothesis H_foo:
— no space before colon after the name of a hypothesis, and the name should start withH_
. -
Lemma foo:
— same here. -
Definition foo (bar_arg : ItsType) : TypeOfDefinition := ...
— again, spaces before explicit types.
My question to you: Do I recall this correctly? Is this what we want(ed) to standardize on?
I guess the only two viable alternatives would be no space before the colon everywhere (as in e.g. Rust), or always place a space before a colon (which looks weird for hypotheses and lemmas IMO).
In any case, we should pick one style and stick to it (and check compliance as part of CI).
Any preferences or opinions, or are you ok with me picking (and ultimately enforcing) something as long as it's consistent?
CC: @proux @sophie @mlesourd @ptorrx @mmaida @sbozhko @pointoflight