Merge PR #8856: [gitlab] Test Ocaml trunk.

7 files changed, 73 insertions, 11 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index de0de4cf83..108ecb5a04 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-12-05-V1"
+  CACHEKEY: "bionic_coq-V2018-12-14-V1"
   IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY"
   # By default, jobs run in the base switch; override to select another switch
   OPAM_SWITCH: "base"
@@ -367,6 +367,57 @@ test-suite:egde:dune:dev:
     paths:
       - _build/default/test-suite/logs
 
+test-suite:edge+trunk+make:
+  stage: test
+  dependencies: []
+  script:
+    - opam switch create 4.08.0 --empty
+    - eval $(opam env)
+    - opam repo add ocaml-pr https://github.com/ocaml/ocaml-pr-repository.git
+    - opam update
+    - opam install ocaml-variants=4.08.0 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: edge
+  artifacts:
+    name: "$CI_JOB_NAME.logs"
+    when: always
+    paths:
+      - test-suite/logs
+    expire_in: 1 week
+  allow_failure: true
+
+test-suite:edge+trunk+dune:
+  stage: test
+  dependencies: []
+  script:
+    - opam switch create 4.08.0 --empty
+    - eval $(opam env)
+    - opam repo add ocaml-pr https://github.com/ocaml/ocaml-pr-repository.git
+    - opam update
+    - opam install ocaml-variants=4.08.0 num
+    - opam pin add dune --dev # ounit lablgtk conf-gtksourceview
+    - opam install dune
+    - 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=ocaml408
+  variables:
+    OPAM_SWITCH: edge
+  artifacts:
+    name: "$CI_JOB_NAME.logs"
+    when: always
+    paths:
+      - _build/log
+      - _build/default/test-suite/logs
+    expire_in: 1 week
+  allow_failure: true
+
 validate:base:
   <<: *validate-template
   dependencies:
diff --git a/Makefile.dune b/Makefile.dune
index 4baf3402f1..22e3271260 100644
--- a/Makefile.dune
+++ b/Makefile.dune
@@ -4,7 +4,7 @@
 .PHONY: help voboot states world watch check          # Main developer targets
 .PHONY: quickbyte quickopt                            # Partial / quick developer targets
 .PHONY: test-suite refman-html apidoc release         # Accesory targets
-.PHONY: ocheck ireport clean                          # Maintenance targets
+.PHONY: ocheck trunk ireport clean                    # Maintenance targets
 
 # use DUNEOPT=--display=short for a more verbose build
 # DUNEOPT=--display=short
@@ -28,6 +28,7 @@ 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"
@@ -75,6 +76,11 @@ release: voboot
 ocheck: voboot
 	dune build $(DUNEOPT) @install --workspace=dev/dune-workspace.all
 
+trunk:
+	dune build $(DUNEOPT) --profile=ocaml408 @vodeps
+	dune exec coq_dune $(BUILD_CONTEXT)/.vfiles.d
+	dune build $(DUNEOPT) --profile=ocaml408 coq.install coqide-server.install
+
 ireport:
 	dune clean
 	dune build $(DUNEOPT) @vodeps --profile=ireport
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index f1020e5f8e..baf470e021 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2018-12-05-V1"
+# CACHEKEY: "bionic_coq-V2018-12-14-V1"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -37,7 +37,7 @@ 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.6.1 ounit.2.0.8 odoc.1.3.0" \
+ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.6.2 ounit.2.0.8 odoc.1.3.0" \
     CI_OPAM="menhir.20180530 elpi.1.1.0 ocamlgraph.1.8.8"
 
 # BASE switch; CI_OPAM contains Coq's CI dependencies.
diff --git a/dune b/dune
index 270738c23c..a7264ba91e 100644
--- a/dune
+++ b/dune
@@ -4,7 +4,9 @@
  (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)))
+          (ocamlopt_flags :standard -O3 -unbox-closures -inlining-report))
+ (ocaml408
+  (flags :standard -strict-sequence -strict-formats -short-paths -keep-locs -rectypes -w -9-27+40+60 -warn-error -5 -alert --deprecated)))
 
 ; The _ profile could help factoring the above, however it doesn't
 ; seem to work like we'd expect/like:
diff --git a/kernel/dune b/kernel/dune
index 4f2e0e4e28..01abdb8f67 100644
--- a/kernel/dune
+++ b/kernel/dune
@@ -18,3 +18,4 @@
 ; warnings.
 (env
  (dev (flags :standard -w +a-4-44-50)))
+ ; (ocaml408 (flags :standard -w +a-3-4-44-50)))
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 530671e1a1..34a1900bbc 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -90,19 +90,17 @@ FAIL = >&2 echo 'FAILED    $@'
 # Testing subsystems
 #######################################################################
 
-# Apart so that it can be easily skipped with overriding
+# These targets can be skipped by doing `make TARGET= test-suite`
 COMPLEXITY := $(if $(bogomips),complexity)
-
 BUGS := bugs/opened bugs/closed
-
 INTERACTIVE := interactive
-
+UNIT_TESTS := unit-tests
 VSUBSYSTEMS := prerequisite success failure $(BUGS) output \
   output-modulo-time $(INTERACTIVE) micromega $(COMPLEXITY) modules stm \
   coqdoc ssr
 
 # All subsystems
-SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile tools unit-tests
+SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile tools $(UNIT_TESTS)
 
 PREREQUISITELOG = prerequisite/admit.v.log			\
   prerequisite/make_local.v.log prerequisite/make_notation.v.log \
@@ -119,6 +117,10 @@ PREREQUISITELOG = prerequisite/admit.v.log			\
 all: run
 	$(MAKE) report
 
+# do nothing
+.PHONY: noop
+noop: ;
+
 run: $(SUBSYSTEMS)
 bugs: $(BUGS)
 
diff --git a/test-suite/dune b/test-suite/dune
index c5fa0bb14a..eae072553a 100644
--- a/test-suite/dune
+++ b/test-suite/dune
@@ -70,4 +70,4 @@
   (progn
    ; XXX: we will allow to set the NJOBS variable in a future Dune
    ; version, either by using an env var or by letting Dune set `-j`
-   (run make -j 2 BIN= PRINT_LOGS=1))))
+   (run make -j 2 BIN= PRINT_LOGS=1 UNIT_TESTS=%{env:COQ_UNIT_TEST=unit-tests}))))