From 7b28475547cc2391034f3e61437777d4513e9094 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 23 Sep 2020 11:11:38 +0200
Subject: Remove the ocamlformat git hook.

---
 dev/tools/pre-commit | 26 +++-----------------------
 1 file changed, 3 insertions(+), 23 deletions(-)

diff --git a/dev/tools/pre-commit b/dev/tools/pre-commit
index 448e224f2e..74fcceb038 100755
--- a/dev/tools/pre-commit
+++ b/dev/tools/pre-commit
@@ -7,25 +7,7 @@ set -e
 
 dev/tools/check-overlays.sh
 
-# Can we check and fix formatting?
-# NB: we will ignore errors from ocamlformat as it fails when
-# encountering OCaml syntax errors
-ocamlformat=$(command -v ocamlformat || echo true)
-if [ "$ocamlformat" = true ]
-then
-    1>&2 echo "Warning: ocamlformat is not in path. Cannot check formatting."
-fi
-
-# Verify that the version of ocamlformat matches the one in .ocamlformat
-# The following command will print an error message if that's not the case
-# (and will print nothing if the versions match)
-if ! echo "let () = ()" | "$ocamlformat" --impl - > /dev/null
-then
-    1>&2 echo "Warning: Cannot check formatting."
-    ocamlformat=true
-fi
-
-1>&2 echo "Auto fixing whitespace and formatting issues..."
+1>&2 echo "Auto fixing whitespace issues..."
 
 # We fix whitespace in the index and in the working tree
 # separately to preserve non-added changes.
@@ -52,7 +34,6 @@ if [ -s "$index" ]; then
     git apply --cached --whitespace=fix "$index"
     git apply --whitespace=fix "$index" 2>/dev/null # no need to repeat yourself
     git diff --cached --name-only -z | xargs -0 dev/tools/check-eof-newline.sh --fix
-    { git diff --cached --name-only -z | grep -E '.*\.mli?$' -z | xargs -0 "$ocamlformat" -i || true; } 2> /dev/null
     git add -u
     1>&2 echo #newline
 fi
@@ -68,12 +49,11 @@ if [ -s "$tree" ]; then
     1>&2 echo "Fixing unstaged changes..."
     git apply --whitespace=fix "$tree"
     git diff --name-only -z | xargs -0 dev/tools/check-eof-newline.sh --fix
-    { git diff --name-only -z | grep -E '.*\.mli?$' -z | xargs -0 "$ocamlformat" -i || true; } 2> /dev/null
     1>&2 echo #newline
 fi
 
 if [ -s "$index" ] && ! [ -s "$fixed_index" ]; then
-    1>&2 echo "Fixing whitespace and formatting issues cancelled all changes."
+    1>&2 echo "Fixing whitespace issues cancelled all changes."
     exit 1
 fi
 
@@ -84,7 +64,7 @@ if ! git diff-index --check --cached HEAD; then
     1>&2 echo "(Consider whether the number of errors decreases after each run.)"
     exit 1
 fi
-1>&2 echo "Whitespace and formatting pass complete."
+1>&2 echo "Whitespace pass complete."
 
 # clean up temporary files
 rm "$index" "$tree" "$fixed_index"
-- 
cgit v1.2.3


From 3a88c57442c0c9a5e23a25d04e3695d6e61587c3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 23 Sep 2020 11:12:44 +0200
Subject: Remove the linter ocamlformat pass.

---
 dev/lint-repository.sh | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/dev/lint-repository.sh b/dev/lint-repository.sh
index 553696410c..2e8a7455de 100755
--- a/dev/lint-repository.sh
+++ b/dev/lint-repository.sh
@@ -32,7 +32,4 @@ find . "(" -path ./.git -prune ")" -o -type f -print0 |
 echo Checking overlays
 dev/tools/check-overlays.sh || CODE=1
 
-echo Checking ocamlformat
-make -f Makefile.dune fmt || CODE=1
-
 exit $CODE
-- 
cgit v1.2.3


From 4a51746571d32516da3aa228ceceb1d8364d058b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 23 Sep 2020 11:13:51 +0200
Subject: Document the ocamlformat changes.

---
 dev/doc/changes.md | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 7d2100515d..59c1623a2d 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -4,6 +4,12 @@
   comes from a notation. Use `None` if not and `Some foo` to tell to
   print such TacGeneric surrounded with `foo:( )`.
 
+### Code formatting
+
+- The automatic code formatting tool `ocamlformat` has been disabled and its
+  git hook removed. If desired, automatic formatting can be achieved by calling
+  the `fmt` target of the dune build system.
+
 ## Changes between Coq 8.11 and Coq 8.12
 
 ### Code formatting
-- 
cgit v1.2.3