Commit Convention
cpehle opened this issue · 5 comments
It has occurred to me that we maybe should adopt some kind of commit convention. I think the one used by Lean4 is pretty good https://github.com/leanprover/lean4/blob/master/doc/dev/commit_convention.md. The core contributors should be able to exercise judgement and bypass review for some categories of commits mentioned there. What do you think @Jegp?
The current situation where we sometimes have relative long living branches is I think slowing us down and clearly distinguishing between types of commits and splitting up work in smaller pieces might help with that.
i think that's a good idea, but I wouldn't enforce it strictly. I think our main problem is, as you hint at, that we don't close issues/PRs. Splitting up work is definitely the way to go, but I'm not sure enforcing strict commit formatting is the only way to Rome. In the worst case, it'll slow us down even more because we spend more time formatting than writing code. I don't think that's the case, but I wanted to highlight that possibility if we're too stringent.
One problem, I think, is that the people (I'm also guilty!) fail to react to the PRs. Perhaps organizing regular hackathons/crunches where we buckle down on open branches would be even more efficient? That's a separate discussion, though.
I'm happy if you would want to push for a commit convention, @cpehle. If you think it's a good idea. Until then, would you be ok to close the issue? We can always reopen it later.
I would be happy to basically adopt the one I referenced above. I think it could be helpful in the future to get a better sense of what is happening at a glance. Looking back at the PR and commit messages, this was not always the case. It also encourages one to keep each commit to one "topic". What do you think?
I think that's a great idea! I don't know exactly how that would look like. Should we just "adopt" their .md file and try to enforce it going forward? Could it be a part of the contribution standards?
Yeah it could be even enforced by a pre-commit hook and a check for each pull request. We would need to acknowledge the source of course, but otherwise I don't think we would necessarily need to deviate to much from it.