Document pre-commit hook and its bypass (issue #236)

docs/developer-guide/developing.md

@@ -0,0 +1,15 @@
+# Developing
+
+Running `make dev` does the following:
+
+1. Installs some additional opam packages useful for developing.
+2. Installs a Git pre-commit hook for ocp-indent (see below).
+
+## Git
+### Pre-commit hook
+The pre-commit hook installed by `make dev` runs ocp-indent on the staged changes to check that they're correctly indented.
+If it deems something incorrectly indented, it will output a diff showing where and how, and it will prevent the commit.
+In VSCode you have to click "Show Command Output" in the error popup to see the diff.
+
+If necessary (e.g. you think ocp-indent is wrong or wants you to fix unrelated code), the hook can be bypassed using `git commit -n`.
+In such case also let us know about the inconvenience on the following GitHub issue, so we can work towards improving the process: <https://github.com/goblint/analyzer/issues/236>.

make.sh

@@ -106,6 +106,7 @@ rule() {
       echo "Be sure to adjust your vim/emacs config!"
       echo "Installing Pre-commit hook..."
       cd .git/hooks; ln -s ../../scripts/hooks/pre-commit; cd -
+      # Use `git commit -n` to temporarily bypass the hook if necessary.
       echo "Installing gem parallel (not needed for ./scripts/update_suite.rb -s)"
       sudo gem install parallel
     ;; headers)

mkdocs.yml

@@ -20,6 +20,7 @@ nav:
     - user-guide/running.md
     - user-guide/inspecting.md
   - 'Developer guide':
+    - developer-guide/developing.md
     - developer-guide/testing.md
     - developer-guide/debugging.md
     - developer-guide/documenting.md

scripts/hooks/pre-commit

@@ -1,5 +1,8 @@
 #!/bin/sh
-#
+
+# Uses ocp-indent to check that staged changes are correctly indented.
+# Use `git commit -n` to bypass if necessary.
+
 # An example hook script to verify what is about to be committed.
 # Called by "git commit" with no arguments.  The hook should
 # exit with non-zero status after issuing an appropriate message if