From 85b91b71abe7e60a9096ae31b9d0b4afda2189bb Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 25 Oct 2018 13:05:36 +0200
Subject: [dune] [gitlab] Test OCaml trunk.

We add a job testing the build of Coq with OCaml 4.08 [AKA `trunk`]

CoqIDE is not supported in 4.08 due to missing `lablgtk`, also `oUnit`
cannot be currently installed, thus we have to add a switch to the
test suite to disable `unit-tests`.

Many deprecation warnings happened in 4.08 so we use the `release`
profile to make them not fatal. Using a 4.08 build profile would be an
option too.
---
 test-suite/Makefile | 12 +++++++-----
 test-suite/dune     |  2 +-
 2 files changed, 8 insertions(+), 6 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/Makefile b/test-suite/Makefile
index 9d2277c37e..d7956db8e6 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}))))
-- 
cgit v1.2.3