diff options
| author | Jason Gross | 2018-09-01 20:05:07 -0400 |
|---|---|---|
| committer | Jason Gross | 2018-10-02 14:48:10 -0400 |
| commit | 425475e4605691642b09b625dd13e7e3506299b6 (patch) | |
| tree | 5044834ad1cf09a85ee2e652ffb8f00e8b63ca04 /test-suite | |
| parent | 3208a68e2c1b5f29fe33b54a66a2c361d3bfc531 (diff) | |
Move the compat-update-process to right after branching
Also test that the compat updating script hasn't become outdated on the
CI.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/Makefile | 23 | ||||
| -rwxr-xr-x | test-suite/tools/update-compat/run.sh | 9 |
2 files changed, 31 insertions, 1 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 93ce519350..bde0bfc91f 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -102,7 +102,7 @@ VSUBSYSTEMS := prerequisite success failure $(BUGS) output \ coqdoc ssr # All subsystems -SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile 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 \ @@ -174,6 +174,7 @@ summary: $(call summary_dir, "Coqwc tests", coqwc); \ $(call summary_dir, "Coq makefile", coq-makefile); \ $(call summary_dir, "Coqdoc tests", coqdoc); \ + $(call summary_dir, "tools/ tests", tools); \ $(call summary_dir, "Unit tests", unit-tests); \ nb_success=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_success) | wc -l`; \ nb_failure=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_failure) | wc -l`; \ @@ -652,3 +653,23 @@ $(addsuffix .log,$(wildcard coqdoc/*.v)): %.v.log: %.v %.html.out %.tex.out $(PR $(FAIL); \ fi; \ } > "$@" + +# tools/ + +tools: $(patsubst %/run.sh,%.log,$(wildcard tools/*/run.sh)) + +tools/%.log : tools/%/run.sh + @echo "TEST tools/$*" + $(HIDE)(\ + export COQBIN=$(BIN);\ + cd tools/$* && \ + bash run.sh 2>&1; \ + if [ $$? = 0 ]; then \ + echo $(log_success); \ + echo " $<...Ok"; \ + else \ + echo $(log_failure); \ + echo " $<...Error!"; \ + $(FAIL); \ + fi; \ + ) > "$@" diff --git a/test-suite/tools/update-compat/run.sh b/test-suite/tools/update-compat/run.sh new file mode 100755 index 0000000000..02a2348450 --- /dev/null +++ b/test-suite/tools/update-compat/run.sh @@ -0,0 +1,9 @@ +#!/usr/bin/env bash + +# allow running this script from any directory by basing things on where the script lives +SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null && pwd )" + +# we assume that the script lives in test-suite/tools/update-compat/, +# and that update-compat.py lives in dev/tools/ +cd "${SCRIPT_DIR}/../../.." +dev/tools/update-compat.py --assert-unchanged --cur-version=8.9 || exit $? |