Merge PR #11257: [dev] [ocaml] Add ocamlformat configuration.

Reviewed-by: Zimmi48

10 files changed, 82 insertions, 8 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 6344b51702..935d5fda84 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-V2019-12-03-V81"
+  CACHEKEY: "bionic_coq-V2019-12-08-V82"
   IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY"
   # By default, jobs run in the base switch; override to select another switch
   OPAM_SWITCH: "base"
@@ -310,7 +310,8 @@ lint:
   dependencies: []
   variables:
     GIT_DEPTH: "" # we need an unknown amount of history for per-commit linting
-    OPAM_SWITCH: base
+    OPAM_SWITCH: "edge"
+    OPAM_VARIANT: "+flambda"
 
 pkg:opam:
   stage: stage-1
diff --git a/.ocamlformat b/.ocamlformat
new file mode 100644
index 0000000000..3c6f577afd
--- /dev/null
+++ b/.ocamlformat
@@ -0,0 +1,6 @@
+profile=ocamlformat
+module-item-spacing=compact
+sequence-style=terminator
+cases-exp-indent=2
+field-space=loose
+exp-grouping=preserve
diff --git a/.ocamlformat-ignore b/.ocamlformat-ignore
new file mode 100644
index 0000000000..af9d896319
--- /dev/null
+++ b/.ocamlformat-ignore
@@ -0,0 +1,52 @@
+configure.ml
+dev/*
+coqpp/*
+lib/*
+clib/*
+config/*
+checker/*
+kernel/*
+library/*
+engine/*
+gramlib/*
+parsing/*
+interp/*
+pretyping/*
+printing/*
+proofs/*
+stm/*
+tactics/*
+theories/*
+user-contrib/*/*
+vernac/*
+toplevel/*
+topbin/*
+ide/*
+ide/*/*
+doc/plugin_tutorial/*/*/*
+doc/tools/docgram/*
+test-suite/*
+test-suite/*/*/*
+test-suite/*/*/*/*
+test-suite/*/*/*/*/*
+tools/*
+tools/*/*
+plugins/btauto/*
+plugins/cc/*
+plugins/derive/*
+plugins/extraction/*
+plugins/firstorder/*
+plugins/fourier/*
+plugins/funind/*
+plugins/ltac/*
+plugins/micromega/*
+plugins/nsatz/*
+plugins/omega/*
+plugins/rtauto/*
+plugins/setoid/*
+plugins/ing/*
+plugins/setoid_ring/*
+plugins/ssr/*
+plugins/ssrmatching/*
+plugins/syntax/*
+# Enabled: none for now
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index e26103cedd..1a12360c13 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -497,6 +497,11 @@ We have a linter that checks a few different things:
   your branch with `git rebase --whitespace=fix`.
 - **All files should end with a single newline**.  See the section
   [Style guide](#style-guide) for additional style recommendations.
+- **Code is properly formatted**: for some parts of the codebase,
+  formatting will be enforced using the
+  [`ocamlformat`](https://github.com/ocaml-ppx/ocamlformat) tool. You
+  can integrate the formatter in your editor of choice (see docs) or
+  use `dune build @fmt --auto-promote` to fix this kind of errors.
 
 You may run the linter yourself with `dev/lint-repository.sh`.
 
diff --git a/default.nix b/default.nix
index 6a7a98aa5e..ee4a6046ea 100644
--- a/default.nix
+++ b/default.nix
@@ -66,7 +66,7 @@ stdenv.mkDerivation rec {
   )
   ++ optionals shell (
     [ jq curl gitFull gnupg ] # Dependencies of the merging script
-    ++ (with ocamlPackages; [ merlin ocp-indent ocp-index utop ]) # Dev tools
+    ++ (with ocamlPackages; [ merlin ocp-indent ocp-index utop ocamlformat ]) # Dev tools
     ++ [ graphviz ] # Useful for STM debugging
   );
 
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 8907843b12..b8f9d99702 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2019-12-03-V81"
+# CACHEKEY: "bionic_coq-V2019-12-08-V82"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -22,7 +22,7 @@ RUN pip3 install sphinx==1.7.8 sphinx_rtd_theme==0.2.5b2 \
                  antlr4-python3-runtime==4.7.1 sphinxcontrib-bibtex==0.4.0
 
 # We need to install OPAM 2.0 manually for now.
-RUN wget https://github.com/ocaml/opam/releases/download/2.0.4/opam-2.0.4-x86_64-linux -O /usr/bin/opam && chmod 755 /usr/bin/opam
+RUN wget https://github.com/ocaml/opam/releases/download/2.0.5/opam-2.0.5-x86_64-linux -O /usr/bin/opam && chmod 755 /usr/bin/opam
 
 # Basic OPAM setup
 ENV NJOBS="2" \
@@ -58,7 +58,7 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \
 # EDGE switch
 ENV COMPILER_EDGE="4.09.0" \
     COQIDE_OPAM_EDGE="cairo2.0.6.1 lablgtk3-sourceview3.3.0.beta6" \
-    BASE_OPAM_EDGE="dune-release.1.3.3"
+    BASE_OPAM_EDGE="dune-release.1.3.3 ocamlformat.0.12"
 
 # EDGE+flambda switch, we install CI_OPAM as to be able to use
 # `ci-template-flambda` with everything.
diff --git a/dev/doc/README.md b/dev/doc/README.md
index bc281e0d94..ba53605b0e 100644
--- a/dev/doc/README.md
+++ b/dev/doc/README.md
@@ -43,8 +43,12 @@ To learn how to run the test suite, you can read
 
 
 ## Development environment + tooling
+
 - [`Merlin`](https://github.com/ocaml/merlin) for autocomplete.
 - [Wiki pages on tooling containing `emacs`, `vim`, and `git` information](https://github.com/coq/coq/wiki/DevelSetup)
+- [`ocamlformat`](https://github.com/ocaml-ppx/ocamlformat) provides
+  support for automatic formatting of OCaml code. To use it please run
+  `dune build @fmt`, see `ocamlformat`'s documentation for more help.
 
 ## A note about rlwrap
 
diff --git a/dev/lint-repository.sh b/dev/lint-repository.sh
index 2e8a7455de..224601bbce 100755
--- a/dev/lint-repository.sh
+++ b/dev/lint-repository.sh
@@ -32,4 +32,7 @@ find . "(" -path ./.git -prune ")" -o -type f -print0 |
 echo Checking overlays
 dev/tools/check-overlays.sh || CODE=1
 
+echo Checking ocamlformat
+dune build @fmt || CODE=1
+
 exit $CODE
diff --git a/dev/nixpkgs.nix b/dev/nixpkgs.nix
index e7a0ba4f6c..677377f868 100644
--- a/dev/nixpkgs.nix
+++ b/dev/nixpkgs.nix
@@ -1,4 +1,4 @@
 import (fetchTarball {
-  url = "https://github.com/NixOS/nixpkgs/archive/4cd2cb43fb3a87f48c1e10bb65aee99d8f24cb9d.tar.gz";
-  sha256 = "1d6rmq67kdg5gmk94wx2774qw89nvbhy6g1f2lms3c9ph37hways";
+  url = "https://github.com/NixOS/nixpkgs/archive/f4ad230f90ef312695adc26f256036203e9c70af.tar.gz";
+  sha256 = "0cdd275dz3q51sknn7s087js81zvaj5riz8f29id6j6chnyikzjq";
 })
diff --git a/dune-project b/dune-project
index 1249c4af9f..fa05f5fb41 100644
--- a/dune-project
+++ b/dune-project
@@ -2,6 +2,9 @@
 (name coq)
 (using coq 0.1)
 
+(formatting
+ (enabled_for ocaml))
+
 ; We cannot set this to true until as long as the build is not
 ; properly bootstrapped [that is, we remove the voboot target]
 ;