Merge PR #11778: [ocamformat] Update to 0.13.0

Reviewed-by: Zimmi48

5 files changed, 19 insertions, 13 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 5e6c380f4b..621374da0e 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -18,7 +18,7 @@ stages:
 variables:
   # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here
   # for reference]
-  CACHEKEY: "bionic_coq-V2020-03-19-V93"
+  CACHEKEY: "bionic_coq-V2020-03-19-V29"
   IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY"
   # By default, jobs run in the base switch; override to select another switch
   OPAM_SWITCH: "base"
diff --git a/.ocamlformat b/.ocamlformat
index 59883180e5..d5608839fb 100644
--- a/.ocamlformat
+++ b/.ocamlformat
@@ -1,3 +1,4 @@
+version=0.13.0
 profile=ocamlformat
 module-item-spacing=compact
 sequence-style=terminator
diff --git a/Makefile.dune b/Makefile.dune
index b433ed1b94..499ad0d16b 100644
--- a/Makefile.dune
+++ b/Makefile.dune
@@ -102,7 +102,7 @@ release: voboot
 	dune build $(DUNEOPT) -p coq
 
 fmt: voboot
-	dune build @fmt
+	dune build @fmt --auto-promote
 
 ocheck: voboot
 	dune build $(DUNEOPT) @install --workspace=dev/dune-workspace.all
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index e14f634073..e56e4d38ea 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2020-03-19-V93"
+# CACHEKEY: "bionic_coq-V2020-03-19-V29"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -57,7 +57,7 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \
 
 # EDGE switch
 ENV COMPILER_EDGE="4.09.1" \
-    BASE_OPAM_EDGE="dune-release.1.3.3 ocamlformat.0.12"
+    BASE_OPAM_EDGE="dune-release.1.3.3 ocamlformat.0.13.0"
 
 # EDGE+flambda switch, we install CI_OPAM as to be able to use
 # `ci-template-flambda` with everything.
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 9088df6856..b82388675c 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -1,19 +1,19 @@
 ## Changes between Coq 8.11 and Coq 8.12
 
-### ML API
+### Code formatting
 
-Refiner.catchable_exception is deprecated, use instead
-CErrors.noncritical in try-with block. Note that nothing is needed in
-tclORELSE block since the exceptions there are supposed to be
-non-critical by construction.
+- The automatic code formatting tool `ocamlformat` is enabled now for
+  the micromega codebase. Version 0.13.0 is required. See
+  `ocalmformat`'s documentation for more details on integration with
+  your editor.
 
 ### ML API
 
-Types `precedence`, `parenRelation`, `tolerability` in
-`notgram_ops.ml` have been reworked. See `entry_level` and
-`entry_relative_level` in `constrexpr.ml`.
+Notations:
 
-### ML API
+- Types `precedence`, `parenRelation`, `tolerability` in
+  `notgram_ops.ml` have been reworked. See `entry_level` and
+  `entry_relative_level` in `constrexpr.ml`.
 
 Exception handling:
 
@@ -28,6 +28,11 @@ Exception handling:
   + printers are of type `exn -> Pp.t option` [`None` == not handled]
   + it is forbidden for exception printers to raise.
 
+- Refiner.catchable_exception is deprecated, use instead
+  CErrors.noncritical in try-with block. Note that nothing is needed in
+  tclORELSE block since the exceptions there are supposed to be
+  non-critical by construction.
+
 Printers:
 
 - Functions such as Printer.pr_lconstr_goal_style_env have been