Merge PR #12972: [ci] [docker] Up testing to OCaml 4.11.1

Reviewed-by: Zimmi48

10 files changed, 33 insertions, 30 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index ca5584bcb5..cfa6f84147 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -19,7 +19,7 @@ stages:
 variables:
   # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here
   # for reference]
-  CACHEKEY: "bionic_coq-V2020-08-28-V92"
+  CACHEKEY: "bionic_coq-V2020-09-07-V22"
   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 a0d4ef6bbb..93f5ab4007 100644
--- a/.ocamlformat
+++ b/.ocamlformat
@@ -1,4 +1,4 @@
-version=0.14.2
+version=0.15.0
 profile=ocamlformat
 
 # to enable a whole directory, put "disable=false" in dir/.ocamlformat
diff --git a/INSTALL.md b/INSTALL.md
index abc38390e0..05a92ca005 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -13,7 +13,7 @@ Build Requirements
 To compile Coq yourself, you need:
 
 - [OCaml](https://ocaml.org/) (version >= 4.05.0)
-  (This version of Coq has been tested up to OCaml 4.10.0)
+  (This version of Coq has been tested up to OCaml 4.11.1)
 
 - The [num](https://github.com/ocaml/num) library; note that it is
   included in the OCaml distribution for OCaml versions < 4.06.0
@@ -53,7 +53,7 @@ CoqIDE with:
 Opam (https://opam.ocaml.org/) is recommended to install OCaml and
 the corresponding packages.
 
-    $ opam switch create coq 4.10.0+flambda
+    $ opam switch create coq 4.11.1+flambda
     $ eval $(opam env)
     $ opam install num ocamlfind lablgtk3-sourceview3
 
diff --git a/azure-pipelines.yml b/azure-pipelines.yml
index 5830095861..17228bda8a 100644
--- a/azure-pipelines.yml
+++ b/azure-pipelines.yml
@@ -84,7 +84,7 @@ jobs:
       opam list
     displayName: 'Install OCaml dependencies'
     env:
-      COMPILER: "4.10.0"
+      COMPILER: "4.11.1"
       FINDLIB_VER: ".1.8.1"
       OPAMYES: "true"
 
diff --git a/dev/ci/azure-opam.sh b/dev/ci/azure-opam.sh
index 17d71ac52a..f2397cdcee 100755
--- a/dev/ci/azure-opam.sh
+++ b/dev/ci/azure-opam.sh
@@ -2,7 +2,7 @@
 
 set -e -x
 
-OPAM_VARIANT=ocaml-variants.4.10.0+mingw64c
+OPAM_VARIANT=ocaml-variants.4.11.1+mingw64c
 
 wget https://github.com/fdopen/opam-repository-mingw/releases/download/0.0.0.2/opam64.tar.xz -O opam64.tar.xz
 tar -xf opam64.tar.xz
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 78c8673299..ee50d25318 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2020-08-28-V92"
+# CACHEKEY: "bionic_coq-V2020-09-07-V22"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -43,7 +43,7 @@ ENV COMPILER="4.05.0"
 # Common OPAM packages, num to be removed once the migration to
 # micromega is complete, `num` also does not have a version number as
 # the right version to install varies with the compiler version.
-ENV BASE_OPAM="num zarith.1.9.1 ocamlfind.1.8.1 ounit2.2.2.3 odoc.1.5.0" \
+ENV BASE_OPAM="num zarith.1.9.1 ocamlfind.1.8.1 ounit2.2.2.3 odoc.1.5.1" \
     CI_OPAM="menhir.20190626 ocamlgraph.1.8.8" \
     BASE_ONLY_OPAM="elpi.1.11.0"
 
@@ -63,8 +63,8 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \
         opam install $BASE_OPAM
 
 # EDGE switch
-ENV COMPILER_EDGE="4.10.0" \
-    BASE_OPAM_EDGE="dune.2.5.1 dune-release.1.3.3 ocamlformat.0.14.2"
+ENV COMPILER_EDGE="4.11.1" \
+    BASE_OPAM_EDGE="dune.2.5.1 dune-release.1.3.3 ocamlformat.0.15.0"
 
 # EDGE+flambda switch, we install CI_OPAM as to be able to use
 # `ci-template-flambda` with everything.
diff --git a/dev/dune-workspace.all b/dev/dune-workspace.all
index d6348a3624..679b3d1f79 100644
--- a/dev/dune-workspace.all
+++ b/dev/dune-workspace.all
@@ -3,5 +3,5 @@
 ; Add custom flags here. Default developer profile is `dev`
 (context (opam (switch 4.05.0)))
 (context (opam (switch 4.05.0+32bit)))
-(context (opam (switch 4.10.0)))
-(context (opam (switch 4.10.0+flambda)))
+(context (opam (switch 4.11.1)))
+(context (opam (switch 4.11.1+flambda)))
diff --git a/dev/nixpkgs.nix b/dev/nixpkgs.nix
index bfb25e72dd..e798645ed0 100644
--- a/dev/nixpkgs.nix
+++ b/dev/nixpkgs.nix
@@ -1,4 +1,4 @@
 import (fetchTarball {
-  url = "https://github.com/NixOS/nixpkgs/archive/17812e653d89c46d68b7b10e290b1c16758f4e47.tar.gz";
-  sha256 = "1zcb70dyfqc8l2ywpbvxmpfshapdi0g365m3rhmwpagqg47pnyxs";
+  url = "https://github.com/NixOS/nixpkgs/archive/3c0e3697520cbe7d9eb3a64bfd87de840bf4aa77.tar.gz";
+  sha256 = "1vx7kyaq0i287dragjgfdj94ggwr3ky2b7bq32l8rkd2k3vc3gl5";
 })
diff --git a/doc/changelog/11-infrastructure-and-dependencies/12972-ocaml+4_11.rst b/doc/changelog/11-infrastructure-and-dependencies/12972-ocaml+4_11.rst
new file mode 100644
index 0000000000..855aa360f1
--- /dev/null
+++ b/doc/changelog/11-infrastructure-and-dependencies/12972-ocaml+4_11.rst
@@ -0,0 +1,4 @@
+- **Added:**
+  Coq is now tested against OCaml 4.11.1
+  (`#12972 <https://github.com/coq/coq/pull/12972>`_,
+  by Emilio Jesus Gallego Arias).
diff --git a/plugins/micromega/sos.ml b/plugins/micromega/sos.ml
index 2b04bb80e2..03d2a2d233 100644
--- a/plugins/micromega/sos.ml
+++ b/plugins/micromega/sos.ml
@@ -80,7 +80,7 @@ let is_zero (d, v) = match v with Empty -> true | _ -> false
 (* Vectors. Conventionally indexed 1..n.                                     *)
 (* ------------------------------------------------------------------------- *)
 
-let vector_0 n = ((n, undefined) : vector)
+let vector_0 n : vector = (n, undefined)
 let dim (v : vector) = fst v
 
 let vector_const c n =
@@ -99,7 +99,7 @@ let vector_of_list l =
 (* Matrices; again rows and columns indexed from 1.                          *)
 (* ------------------------------------------------------------------------- *)
 
-let matrix_0 (m, n) = (((m, n), undefined) : matrix)
+let matrix_0 (m, n) : matrix = ((m, n), undefined)
 let dimensions (m : matrix) = fst m
 
 let matrix_cmul c (m : matrix) =
@@ -107,7 +107,7 @@ let matrix_cmul c (m : matrix) =
   if c =/ Q.zero then matrix_0 (i, j)
   else ((i, j), mapf (fun x -> c */ x) (snd m))
 
-let matrix_neg (m : matrix) = ((dimensions m, mapf Q.neg (snd m)) : matrix)
+let matrix_neg (m : matrix) : matrix = (dimensions m, mapf Q.neg (snd m))
 
 let matrix_add (m1 : matrix) (m2 : matrix) =
   let d1 = dimensions m1 and d2 = dimensions m2 in
@@ -138,7 +138,7 @@ let diagonal (v : vector) =
 (* Monomials.                                                                *)
 (* ------------------------------------------------------------------------- *)
 let monomial_1 = (undefined : monomial)
-let monomial_var x = (x |=> 1 : monomial)
+let monomial_var x : monomial = x |=> 1
 
 let (monomial_mul : monomial -> monomial -> monomial) =
   combine ( + ) (fun x -> false)
@@ -152,16 +152,16 @@ let monomial_variables m = dom m
 (* ------------------------------------------------------------------------- *)
 let poly_0 = (undefined : poly)
 let poly_isconst (p : poly) = foldl (fun a m c -> m = monomial_1 && a) true p
-let poly_var x = (monomial_var x |=> Q.one : poly)
+let poly_var x : poly = monomial_var x |=> Q.one
 let poly_const c = if c =/ Q.zero then poly_0 else monomial_1 |=> c
 
 let poly_cmul c (p : poly) =
   if c =/ Q.zero then poly_0 else mapf (fun x -> c */ x) p
 
-let poly_neg (p : poly) = (mapf Q.neg p : poly)
+let poly_neg (p : poly) : poly = mapf Q.neg p
 
-let poly_add (p1 : poly) (p2 : poly) =
-  (combine ( +/ ) (fun x -> x =/ Q.zero) p1 p2 : poly)
+let poly_add (p1 : poly) (p2 : poly) : poly =
+  combine ( +/ ) (fun x -> x =/ Q.zero) p1 p2
 
 let poly_sub p1 p2 = poly_add p1 (poly_neg p2)
 
@@ -1191,14 +1191,13 @@ let sumofsquares_general_symmetry tool pol =
   let diagents =
     end_itlist equation_add (List.map (fun i -> apply allassig (i, i)) (1 -- n))
   in
-  let mk_matrix v =
-    ( ( (n, n)
-      , foldl
-          (fun m (i, j) ass ->
-            let c = tryapplyd ass v Q.zero in
-            if c =/ Q.zero then m else ((j, i) |-> c) (((i, j) |-> c) m))
-          undefined allassig )
-      : matrix )
+  let mk_matrix v : matrix =
+    ( (n, n)
+    , foldl
+        (fun m (i, j) ass ->
+          let c = tryapplyd ass v Q.zero in
+          if c =/ Q.zero then m else ((j, i) |-> c) (((i, j) |-> c) m))
+        undefined allassig )
   in
   let mats = List.map mk_matrix qvars
   and obj =