docs: add a guide for commit messages

[lsf37]

Add a guide for how to write commit messages and commit message tags to make the messages more consistent and to help new people on the project get started more quickly.

[lsf37]

The list of currently used tags is generated from the repo and probably still contains some few that are inconsistent or unwanted. Help appreciated in weeding these out.

[michaelmcinerney]

Just some small nitpicks. But this looks very good and is very helpful. Especially for newcomers. Thanks Gerwin

[corlewis]

One thing I'm not sure about for the tags, are we more interested in the intention behind the commits or the specific files changed?
For example, let's say that we're making a change to lib and are then updating the rest of the proofs as required. However, it turns out that the only change needed is in proof/refine/ARM. In this case, which tag would be more useful, proof or arm refine?
I can see arguments for either, the latter is more useful for seeing which part of the repository have or have not changed, but it also implies more relevance than actually exists and could be distracting in the git history.

[lsf37]

One thing I'm not sure about for the tags, are we more interested in the intention behind the commits or the specific files changed? For example, let's say that we're making a change to lib and are then updating the rest of the proofs as required. However, it turns out that the only change needed is in proof/refine/ARM. In this case, which tag would be more useful, proof or arm refine? I can see arguments for either, the latter is more useful for seeing which part of the repository have or have not changed, but it also implies more relevance than actually exists and could be distracting in the git history.

Generally we want the intention. If it's cheap it's also good to be specific, though, because like you said it enables one to quickly see what has not changed. So in this specific case, I'd go for arm refine, but I'm open to arguments against.

[corlewis]

Thanks for writing this up, it should be very helpful in us keeping a useful git history!

[Xaphiosis]

I don't know if more emphasis is needed on not being lazy and/or doing header-only commits because they're "obvious". In theory yes, in practice would it really help ...

[lsf37]

The paragraph is probably long enough. I don't think more emphasis would achieve much.

[Xaphiosis]

There's another thing to consider on the line below, when to not combine lib and proof changes. I sometimes want to git show the commit to see what was the relevant library change, and not see every update that could go into a proof: update for <whatever lib changes>.
This is not a clear-cut line, because it means there is a broken commit between the two, but it's very useful and our proofs can't really be bisected anyway due to the horrible runtime. I'm interested in people's thoughts on this.

[lsf37]

I'd leave this outside the commit message guide, because it's more a question of what commits one should make. If the proof upadte is small, I think combining them makes sense, but if the proof update is large I also like the split version better, because it enables you to figure out more easily what content has actually changed in the spec.

[Xaphiosis]

I think this is excellent, especially given the very short production timeframe (and no comma/just avalanche!
Added thoughts for discussion now that I had a sec, and I second Gerwin's opinion about intention and tagging above.

[lsf37]

Have addressed the feedback and am planning to merge when the tests are through. Still happy to discuss further changes, the content is not set in stone.