Merge PR #10768: [ci] Update to OCaml 4.09.0, drop now useless "trunk" jobs.

Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48

10 files changed, 20 insertions, 84 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 8b37403960..f0403a7318 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-07-09-V01"
+  CACHEKEY: "bionic_coq-V2019-09-20-V01"
   IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY"
   # By default, jobs run in the base switch; override to select another switch
   OPAM_SWITCH: "base"
@@ -507,62 +507,6 @@ test-suite:egde:dune:dev:
     # Gitlab doesn't support yet "expire_in: never" so we use the instance default
     # expire_in: never
 
-test-suite:edge+trunk+make:
-  stage: stage-1
-  dependencies: []
-  script:
-    - opam switch create 4.09.0 --empty
-    - eval $(opam env)
-    - opam repo add ocaml-beta https://github.com/ocaml/ocaml-beta-repository.git
-    - opam update
-    - opam install ocaml-variants=4.09.0+trunk
-    - opam pin add -n ocamlfind --dev
-    - opam install num
-    - eval $(opam env)
-    # We avoid problems with warnings:
-    - ./configure -profile devel -warn-error no
-    - make -j "$NJOBS" world
-    - make -j "$NJOBS" test-suite UNIT_TESTS=
-  variables:
-    OPAM_SWITCH: base
-  artifacts:
-    name: "$CI_JOB_NAME.logs"
-    when: always
-    paths:
-      - test-suite/logs
-    expire_in: 1 week
-  allow_failure: true
-  only: *full-ci
-
-test-suite:edge+trunk+dune:
-  stage: stage-1
-  dependencies: []
-  script:
-    - opam switch create 4.09.0 --empty
-    - eval $(opam env)
-    - opam repo add ocaml-beta https://github.com/ocaml/ocaml-beta-repository.git
-    - opam update
-    - opam install ocaml-variants=4.09.0+trunk
-    - opam pin add -n ocamlfind --dev
-    - opam pin add dune --dev # ounit lablgtk conf-gtksourceview
-    - opam install dune num
-    - eval $(opam env)
-    # We use the release profile to avoid problems with warnings
-    - make -f Makefile.dune trunk
-    - export COQ_UNIT_TEST=noop
-    - dune runtest --profile=ocaml409
-  variables:
-    OPAM_SWITCH: base
-  artifacts:
-    name: "$CI_JOB_NAME.logs"
-    when: always
-    paths:
-      - _build/log
-      - _build/default/test-suite/logs
-    expire_in: 1 week
-  allow_failure: true
-  only: *full-ci
-
 test-suite:base+async:
   extends: .test-suite-template
   dependencies:
diff --git a/INSTALL b/INSTALL
index e82ecf68f8..e30706e005 100644
--- a/INSTALL
+++ b/INSTALL
@@ -9,7 +9,7 @@ WHAT DO YOU NEED ?
 
    - OCaml (version >= 4.05.0)
      (available at https://ocaml.org/)
-     (This version of Coq has been tested up to OCaml 4.08.1)
+     (This version of Coq has been tested up to OCaml 4.09.0)
 
    - The Num package, which used to be part of the OCaml standard library,
      if you are using an OCaml version >= 4.06.0
diff --git a/Makefile.dune b/Makefile.dune
index 88055d62dc..19e8a770bd 100644
--- a/Makefile.dune
+++ b/Makefile.dune
@@ -6,7 +6,7 @@
 .PHONY: quickbyte quickopt quickide                   # Partial / quick developer targets
 .PHONY: refman-html stdlib-html apidoc                # Documentation targets
 .PHONY: test-suite release                            # Accessory targets
-.PHONY: ocheck trunk ireport clean                    # Maintenance targets
+.PHONY: ocheck ireport clean                          # Maintenance targets
 
 # use DUNEOPT=--display=short for a more verbose build
 # DUNEOPT=--display=short
@@ -36,7 +36,6 @@ help:
 	@echo "  - release:     build Coq in release mode"
 	@echo ""
 	@echo "  - ocheck:  build for all supported OCaml versions [requires OPAM]"
-	@echo "  - trunk:   build with a configuration compatible with OCaml trunk"
 	@echo "  - ireport: build with optimized flambda settings and emit an inline report"
 	@echo "  - clean:   remove build directory and autogenerated files"
 	@echo "  - help:    show this message"
@@ -103,11 +102,6 @@ release: voboot
 ocheck: voboot
 	dune build $(DUNEOPT) @install --workspace=dev/dune-workspace.all
 
-trunk:
-	dune build $(DUNEOPT) --profile=ocaml409 @vodeps
-	dune exec coq_dune $(BUILD_CONTEXT)/.vfiles.d
-	dune build $(DUNEOPT) --profile=ocaml409 coq.install coqide-server.install
-
 ireport:
 	dune clean
 	dune build $(DUNEOPT) @vodeps --profile=ireport
diff --git a/azure-pipelines.yml b/azure-pipelines.yml
index 84f080cc73..38ea915f3c 100644
--- a/azure-pipelines.yml
+++ b/azure-pipelines.yml
@@ -72,8 +72,8 @@ jobs:
       opam list
     displayName: 'Install OCaml dependencies'
     env:
-      COMPILER: "4.08.1"
-      FINDLIB_VER: ".1.8.0"
+      COMPILER: "4.09.0"
+      FINDLIB_VER: ".1.8.1"
       OPAMYES: "true"
 
   - script: |
diff --git a/clib/hashset.ml b/clib/hashset.ml
index debfc15c9a..b7a245aed1 100644
--- a/clib/hashset.ml
+++ b/clib/hashset.ml
@@ -118,8 +118,8 @@ module Make (E : EqType) =
         t.table.(t.rover) <- emptybucket;
         t.hashes.(t.rover) <- [| |];
       end else begin
-        Obj.truncate (Obj.repr bucket) (prev_len + 1);
-        Obj.truncate (Obj.repr hbucket) prev_len;
+        Obj.truncate (Obj.repr bucket) (prev_len + 1) [@ocaml.alert "--deprecated"];
+        Obj.truncate (Obj.repr hbucket) prev_len [@ocaml.alert "--deprecated"];
       end;
       if len > t.limit && prev_len <= t.limit then t.oversize <- t.oversize - 1;
     end;
diff --git a/dev/ci/azure-opam.sh b/dev/ci/azure-opam.sh
index 03ce5a6b5d..ee6c62673b 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.08.1+mingw64c
+OPAM_VARIANT=ocaml-variants.4.09.0+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 567f0539ab..edca83c6ef 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2019-07-09-V01"
+# CACHEKEY: "bionic_coq-V2019-09-20-V01"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -37,12 +37,12 @@ ENV COMPILER="4.05.0"
 # 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 dune.1.10.0 ounit.2.0.8 odoc.1.4.0" \
+ENV BASE_OPAM="num ocamlfind.1.8.1 dune.1.11.3 ounit.2.0.8 odoc.1.4.2" \
     CI_OPAM="menhir.20190626 ocamlgraph.1.8.8" \
     BASE_ONLY_OPAM="elpi.1.7.0"
 
 # BASE switch; CI_OPAM contains Coq's CI dependencies.
-ENV COQIDE_OPAM="cairo2.0.6 lablgtk3-sourceview3.3.0.beta5"
+ENV COQIDE_OPAM="cairo2.0.6.1 lablgtk3-sourceview3.3.0.beta6"
 
 # Must add this to COQIDE_OPAM{,_EDGE} when we update the opam
 # packages "lablgtk3-gtksourceview3"
@@ -56,9 +56,9 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \
     opam install $BASE_OPAM
 
 # EDGE switch
-ENV COMPILER_EDGE="4.08.1" \
-    COQIDE_OPAM_EDGE="cairo2.0.6 lablgtk3-sourceview3.3.0.beta6" \
-    BASE_OPAM_EDGE="dune-release.1.3.1"
+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.2"
 
 # 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 7e53f13e45..28e8773e25 100644
--- a/dev/dune-workspace.all
+++ b/dev/dune-workspace.all
@@ -1,7 +1,7 @@
-(lang dune 1.4)
+(lang dune 1.10)
 
 ; 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.08.1)))
-(context (opam (switch 4.08.1+flambda)))
+(context (opam (switch 4.09.0)))
+(context (opam (switch 4.09.0+flambda)))
diff --git a/dune b/dune
index 6fb0612e4e..832c864fc3 100644
--- a/dune
+++ b/dune
@@ -4,9 +4,7 @@
  (release (flags :standard -rectypes)
           (ocamlopt_flags -O3 -unbox-closures))
  (ireport (flags :standard -rectypes -w -9-27-40+60)
-          (ocamlopt_flags :standard -O3 -unbox-closures -inlining-report))
- (ocaml409
-  (flags :standard -strict-sequence -strict-formats -keep-locs -rectypes -w -9-27+40+60 -warn-error -5 -alert --deprecated)))
+          (ocamlopt_flags :standard -O3 -unbox-closures -inlining-report)))
 
 ; Information about flags for release mode:
 ;
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index e54118c775..f788832d5b 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -96,14 +96,14 @@ let mk_accu (a : atom) : t =
     else
       let data = { data with acc_arg = x :: data.acc_arg } in
       let ans = Obj.repr (accumulate data) in
-      let () = Obj.set_tag ans accumulate_tag in
+      let () = Obj.set_tag ans accumulate_tag [@ocaml.alert "--deprecated"] in
       ans
   in
   let acc = { acc_atm = a; acc_arg = [] } in
   let ans = Obj.repr (accumulate acc) in
   (** FIXME: use another representation for accumulators, this causes naked
       pointers. *)
-  let () = Obj.set_tag ans accumulate_tag in
+  let () = Obj.set_tag ans accumulate_tag [@ocaml.alert "--deprecated"] in
   (Obj.obj ans : t)
 
 let get_accu (k : accumulator) =