From 71872341b12cc793c155f240d055c54690bca43b Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 26 May 2021 09:20:47 +0300 Subject: [PATCH] Document pre-commit hook and its bypass (issue #236) --- docs/developer-guide/developing.md | 15 +++++++++++++++ make.sh | 1 + mkdocs.yml | 1 + scripts/hooks/pre-commit | 5 ++++- 4 files changed, 21 insertions(+), 1 deletion(-) create mode 100644 docs/developer-guide/developing.md diff --git a/docs/developer-guide/developing.md b/docs/developer-guide/developing.md new file mode 100644 index 0000000000..693c9d03fc --- /dev/null +++ b/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: . diff --git a/make.sh b/make.sh index 8cd444e603..d3c735335e 100755 --- a/make.sh +++ b/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) diff --git a/mkdocs.yml b/mkdocs.yml index 02d85f7907..2d517c590f 100644 --- a/mkdocs.yml +++ b/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 diff --git a/scripts/hooks/pre-commit b/scripts/hooks/pre-commit index 4c965ddd01..8f80dd3344 100755 --- a/scripts/hooks/pre-commit +++ b/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