Merge PR #7871: [ci] Upgrade edge OCaml to 4.07.0 and Dune to 1.0.0

8 files changed, 26 insertions, 22 deletions

diff --git a/.circleci/config.yml b/.circleci/config.yml
index 950674b34..adab42c62 100644
--- a/.circleci/config.yml
+++ b/.circleci/config.yml
@@ -11,7 +11,7 @@ defaults:
       - image: $CI_REGISTRY_IMAGE:$CACHEKEY
 
   environment: &envvars
-    CACHEKEY: "bionic_coq-V2018-07-02-V4"
+    CACHEKEY: "bionic_coq-V2018-07-11-V2"
     CI_REGISTRY_IMAGE: registry.gitlab.com/coq/coq
 
 version: 2
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 7c451af26..0ad68b508 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -9,7 +9,7 @@ stages:
 variables:
   # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here
   # for reference]
-  CACHEKEY: "bionic_coq-V2018-07-02-V4"
+  CACHEKEY: "bionic_coq-V2018-07-11-V2"
   IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY"
   # By default, jobs run in the base switch; override to select another switch
   OPAM_SWITCH: "base"
diff --git a/.travis.yml b/.travis.yml
index ce178c8a6..3301d97ce 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -39,13 +39,14 @@ env:
   - NJOBS=2
   # system is == 4.02.3
   - COMPILER="system"
-  - COMPILER_BE="4.06.1"
+  - COMPILER_BE="4.07.0"
+  - DUNE_VER=".1.0.0"
   - CAMLP5_VER=".6.14"
-  - CAMLP5_VER_BE=".7.05"
+  - CAMLP5_VER_BE=".7.06"
   - FINDLIB_VER=".1.4.1"
   - FINDLIB_VER_BE=".1.8.0"
-  - LABLGTK="lablgtk.2.18.3 lablgtk-extras.1.6"
-  - LABLGTK_BE="lablgtk.2.18.6 lablgtk-extras.1.6"
+  - LABLGTK="lablgtk.2.18.3 conf-gtksourceview.2"
+  - LABLGTK_BE="lablgtk.2.18.6 conf-gtksourceview.2"
   - NATIVE_COMP="yes"
   - COQ_DEST="-local"
   - MAIN_TARGET="world"
@@ -196,8 +197,9 @@ matrix:
     - os: osx
       env:
       - TEST_TARGET="test-suite"
-      - COMPILER="4.02.3"
-      - CAMLP5_VER=".6.17"
+      - COMPILER="${COMPILER_BE}"
+      - FINDLIB_VER="${FINDLIB_VER_BE}"
+      - CAMLP5_VER="${CAMLP5_VER_BE}"
       - NATIVE_COMP="no"
       - COQ_DEST="-local"
       - EXTRA_OPAM="ounit"
@@ -211,12 +213,13 @@ matrix:
       osx_image: xcode7.3
       env:
       - TEST_TARGET=""
-      - COMPILER="4.02.3"
-      - CAMLP5_VER=".6.17"
+      - COMPILER="${COMPILER_BE}"
+      - FINDLIB_VER="${FINDLIB_VER_BE}"
+      - CAMLP5_VER="${CAMLP5_VER_BE}"
       - NATIVE_COMP="no"
       - COQ_DEST="-prefix ${PWD}/_install"
       - EXTRA_CONF="-coqide opt -warn-error yes"
-      - EXTRA_OPAM="${LABLGTK}"
+      - EXTRA_OPAM="${LABLGTK_BE}"
       before_install:
       - brew update
       - brew unlink python
@@ -246,7 +249,7 @@ install:
 - opam switch "$COMPILER" && opam update
 - eval $(opam config env)
 - opam config list
-- opam install -j ${NJOBS} -y num ocamlfind${FINDLIB_VER} jbuilder camlp5${CAMLP5_VER} ${EXTRA_OPAM}
+- opam install -j ${NJOBS} -y num ocamlfind${FINDLIB_VER} dune${DUNE_VER} camlp5${CAMLP5_VER} ${EXTRA_OPAM}
 - opam list
 
 script:
diff --git a/INSTALL b/INSTALL
index eabc729f7..6e7903a66 100644
--- a/INSTALL
+++ b/INSTALL
@@ -29,8 +29,9 @@ WHAT DO YOU NEED ?
 
    To compile Coq yourself, you need:
 
-   - OCaml version 4.02.3 or later
+   - OCaml (version >= 4.02.3)
      (available at https://ocaml.org/)
+     (This version of Coq has been tested up to OCaml 4.07.0)
 
    - The Num package, which used to be part of the OCaml standard library,
      if you are using an OCaml version >= 4.06.0
@@ -68,7 +69,7 @@ WHAT DO YOU NEED ?
    profit from Flambda, a special build of the OCaml compiler that has
    the Flambda optimizer enabled must be installed. For OPAM users,
    this amounts to installing a compiler switch ending in `+flambda`,
-   such as `4.06.1+flambda`. For other users, YMMV. Once `ocamlopt
+   such as `4.07.0+flambda`. For other users, YMMV. Once `ocamlopt
    -config` reports that Flambda is available, some further
    optimization options can be used; see the entry about -flambda-opts
    below for more details.
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 94e90bf4f..da5ac2b15 100644
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -793,7 +793,7 @@ function make_ln {
 
 function make_ocaml {
   get_flex_dll_link_bin
-  if build_prep http://caml.inria.fr/pub/distrib/ocaml-4.06 ocaml-4.06.1 tar.gz 1 ; then
+  if build_prep http://caml.inria.fr/pub/distrib/ocaml-4.07 ocaml-4.07.0 tar.gz 1 ; then
     # See README.win32.adoc
     cp config/m-nt.h byterun/caml/m.h
     cp config/s-nt.h byterun/caml/s.h
@@ -933,7 +933,7 @@ function make_camlp5 {
   make_ocaml
   make_findlib
 
-  if build_prep https://github.com/camlp5/camlp5/archive rel705 tar.gz 1 camlp5-rel705; then
+  if build_prep https://github.com/camlp5/camlp5/archive rel706 tar.gz 1 camlp5-rel706; then
     logn configure ./configure
     # Somehow my virus scanner has the boot.new/SAVED directory locked after the move for a second => repeat until success
     sed -i 's/mv boot.new boot/until mv boot.new boot; do sleep 1; done/' Makefile
diff --git a/dev/ci/appveyor.sh b/dev/ci/appveyor.sh
index 7bf9ad8c9..d2176e326 100644
--- a/dev/ci/appveyor.sh
+++ b/dev/ci/appveyor.sh
@@ -2,7 +2,7 @@
 
 set -e -x
 
-APPVEYOR_OPAM_SWITCH=4.06.1+mingw64c
+APPVEYOR_OPAM_SWITCH=4.07.0+mingw64c
 
 wget https://github.com/fdopen/opam-repository-mingw/releases/download/0.0.0.1/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 a4ee6a379..1361392dc 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2018-07-02-V4"
+# CACHEKEY: "bionic_coq-V2018-07-11-V2"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -28,7 +28,7 @@ RUN opam init -a -y -j $NJOBS --compiler="$COMPILER" default https://opam.ocaml.
 # Common OPAM packages.
 # `num` does not have a version number as the right version to install varies
 # with the compiler version.
-ENV BASE_OPAM="num ocamlfind.1.8.0 jbuilder.1.0+beta20 ounit.2.0.8" \
+ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.0.0 ounit.2.0.8" \
     CI_OPAM="menhir.20180530 elpi.1.0.4 ocamlgraph.1.8.8"
 
 # BASE switch; CI_OPAM contains Coq's CI dependencies.
@@ -43,8 +43,8 @@ RUN opam switch -y -j $NJOBS "${COMPILER}+32bit" && eval $(opam config env) && \
     opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER
 
 # EDGE switch
-ENV COMPILER_EDGE="4.06.1" \
-    CAMLP5_VER_EDGE="7.05" \
+ENV COMPILER_EDGE="4.07.0" \
+    CAMLP5_VER_EDGE="7.06" \
     COQIDE_OPAM_EDGE="lablgtk.2.18.6 conf-gtksourceview.2"
 
 RUN opam switch -y -j $NJOBS $COMPILER_EDGE && eval $(opam config env) && \
diff --git a/dev/doc/README.md b/dev/doc/README.md
index 1a4e40f68..223cf6286 100644
--- a/dev/doc/README.md
+++ b/dev/doc/README.md
@@ -7,7 +7,7 @@ Assuming one is running Ubuntu (if not, replace `apt` with the package manager o
 ```
 $ sudo apt-get install make opam git
 
-# At the time of writing, <latest-ocaml-version> is 4.06.1.
+# At the time of writing, <latest-ocaml-version> is 4.07.0.
 # The latest version number is available at: https://ocaml.org/releases/
 
 $ opam init --comp <latest-ocaml-version>