[squash address review feedback

Co-authored-by: Corey Lewis <[email protected]>
Signed-off-by: Gerwin Klein <[email protected]>

docs/commit-messages.md

@@ -35,7 +35,7 @@ with the following exceptions and additions:
 
 - header can be max 78 characters
 - body is wrapped at 78 characters
-- we use tags in the header to in indicate which part of the repository
+- we use tags in the header to indicate which part of the repository
   the commit applies to
 
 We are using 78 for the header because of the tags, which take up some space. If
@@ -59,7 +59,7 @@ You should read it, it's not long and it's good advice.
 Repeating some high-level points:
 
 - Use imperative voice (e.g. `proofs: rename lemma foo to bar`)
-- The header should be a short summary, focussing on "what"
+- The header should be a short summary, focusing on "what"
 - The body should explain what is going on in more detail (also in imperative
   voice), but much more importantly *why* it is going on (is `bar` more
   consistent than `foo`? Is the name `foo` needed for something else? Does `bar`
@@ -74,7 +74,7 @@ Repeating some high-level points:
 - We use tags to indicate which part of the repository the commit applies to,
   and if it is architecture-specific, then to which architecture it applies to.
 
-- We do no usually use branch tags, because git branches are ephemeral and we
+- We do not usually use branch tags, because git branches are ephemeral and we
   are using rebase branches for most of our work. The one exception is the `rt`
   branch, which has been alive for over half a decade. For this branch, we allow
   merge commits (from branch `master` into `rt` only), and we want to be able to
@@ -139,7 +139,7 @@ For all of these, you can supply a path to restrict the log to a certain file
 or directory in the repo. You can also supply a branch, or a commit range like
 `master..rt` to restrict the output.
 
-Esp `git log --oneline` is useful for quickly getting an overview. Example
+Especially `git log --oneline` is useful for quickly getting an overview. Example
 output:
 
 ```
@@ -166,8 +166,8 @@ d0bab9c79 misc/scripts: remove Darwin cpp wrapper
 You can very quickly see that C verification has been active recently, that
 new tests were added, that AARCH64 proofs have been done, and that there was
 some work to do with the AFP and the monad library. You can see that nothing
-has happened with system initialiser or other user-level proofs, and that there
-are no changes that should affect for instance the C parser.
+has happened with the system initialiser or other user-level proofs, and that there
+are no changes that should affect, for instance, the C parser.
 
 You only see such things quickly when the messages are consistent and follow the
 same kind of pattern. It's not so important what the pattern is. It is important
@@ -214,7 +214,6 @@ aarch64 cspec
 aarch64 design
 aarch64 design+machine
 aarch64 haskell
-aarch64 haskell+aspec
 aarch64 haskell+design
 aarch64 haskell+machine
 aarch64 machine+ainvs
@@ -236,8 +235,6 @@ arm infoflow
 arm refine
 arm+arm-hyp crefine
 arm+arm-hyp machine
-arm+arm_hyp crefine
-arm+arm_hyp machine
 arm-hyp aspec
 arm-hyp aspec+design
 arm-hyp ainvs
@@ -246,7 +243,6 @@ arm-hyp design
 arm-hyp haskell
 arm-hyp haskell+refine
 arm-hyp machine
-arm-hyp proofs+ROOT
 arm-hyp refine
 asmrefine
 aspec
@@ -256,11 +252,9 @@ aspec+design+haskell
 aspec+haskell
 autocorres
 bisim
-c-kernel
 c-parser
 c-parser+autocorres
 c-parser+crefine
-c-parser+crefine+clib
 camkes
 capDL
 ckernel
@@ -372,11 +366,9 @@ x64 crefine
 x64 design
 x64 design/skel
 x64 haskell
-x64 invs
 x64 machine
 x64 refine
 x64 refine+crefine
-x64 spec
 ```
 
 Most of these could be prefixed with `rt` if they only made sense on the `rt`