diff options
| author | Emilio Jesus Gallego Arias | 2018-10-25 13:05:36 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-12-14 16:04:35 +0100 |
| commit | 85b91b71abe7e60a9096ae31b9d0b4afda2189bb (patch) | |
| tree | 5bf4f7bcc6be4837dee7c0a946969beb36091946 /test-suite | |
| parent | 40aac459c94b9a8696e4d23dfdc0ce9279e63616 (diff) | |
[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.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/Makefile | 12 | ||||
| -rw-r--r-- | test-suite/dune | 2 |
2 files changed, 8 insertions, 6 deletions
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})))) |