diff options
| -rw-r--r-- | .github/CODEOWNERS | 1 | ||||
| -rw-r--r-- | dev/doc/release-process.md | 58 | ||||
| -rw-r--r-- | test-suite/Makefile | 23 | ||||
| -rwxr-xr-x | test-suite/tools/update-compat/run.sh | 9 |
4 files changed, 61 insertions, 30 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 29fe3ef20b..7ca407f36f 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -352,4 +352,5 @@ # Secondary maintainer @maximedenes /dev/tools/update-compat.py @JasonGross +/test-suite/tools/update-compat/ @JasonGross # Secondary maintainer @Zimmi48 diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md index 7765d4b05c..b33a1cbd73 100644 --- a/dev/doc/release-process.md +++ b/dev/doc/release-process.md @@ -6,6 +6,35 @@ the present checklist. - [ ] Change the version name to the next major version and the magic numbers (see [#7008](https://github.com/coq/coq/pull/7008/files)). +- [ ] Update the compatibility infrastructure, which consists of doing + the following steps. Note that all but the final step can be + performed automatically by + [`dev/tools/update-compat.py`](/dev/tools/update-compat.py) so + long as you have already updated `coq_version` in + [`configure.ml`](/configure.ml). + + [ ] Add a file `theories/Compat/CoqXX.v` which contains just the header + from [`dev/header.ml`](/dev/header.ml) + + [ ] Add the line `Require Export Coq.Compat.CoqXX.` at the top of + `theories/Compat/CoqYY.v`, where Y.Y is the version prior to X.X. + + [ ] Delete the file `theories/Compat/CoqWW.v`, where W.W is three versions + prior to X.X. + + [ ] Update + [`doc/stdlib/index-list.html.template`](/doc/stdlib/index-list.html.template) + with the deleted/added files. + + [ ] Remove any notations in the standard library which have `compat "W.W"`. + + [ ] Update the type `compat_version` in [`lib/flags.ml`](/lib/flags.ml) by + bumping all the version numbers by one, and update the interpretations + of those flags in [`toplevel/coqargs.ml`](/toplevel/coqargs.ml) and + [`vernac/g_vernac.mlg`](/vernac/g_vernac.mlg). + + [ ] Update the files + [`test-suite/success/CompatCurrentFlag.v`](/test-suite/success/CompatCurrentFlag.v), + [`test-suite/success/CompatPreviousFlag.v`](/test-suite/success/CompatPreviousFlag.v), + and + [`test-suite/success/CompatOldFlag.v`](/test-suite/success/CompatOldFlag.v) + by bumping all version numbers by 1. + + [ ] Decide what to do about all test-suite files which mention `-compat + W.W` or `Coq.Comapt.CoqWW` (which is no longer valid, since we only + keep compatibility against the two previous versions) - [ ] Put the corresponding alpha tag using `git tag -s`. The `VX.X+alpha` tag marks the first commit to be in `master` and not in the branch of the previous version. @@ -57,35 +86,6 @@ ## Before the beta release date ## - [ ] Ensure the Credits chapter has been updated. -- [ ] Ensure the compatibility infrastructure has been updated, which consists - of the following steps. Note that all but the final step can be - performed automatically by - [`dev/tools/update-compat.py`](/dev/tools/update-compat.py) so long as - you have already updated `coq_version` in - [`configure.ml`](/configure.ml). - + [ ] Add a file `theories/Compat/CoqXX.v` which contains just the header - from [`dev/header.ml`](/dev/header.ml) - + [ ] Add the line `Require Export Coq.Compat.CoqXX.` at the top of - `theories/Compat/CoqYY.v`, where Y.Y is the version prior to X.X. - + [ ] Delete the file `theories/Compat/CoqWW.v`, where W.W is three versions - prior to X.X. - + [ ] Update - [`doc/stdlib/index-list.html.template`](/doc/stdlib/index-list.html.template) - with the deleted/added files. - + [ ] Remove any notations in the standard library which have `compat "W.W"`. - + [ ] Update the type `compat_version` in [`lib/flags.ml`](/lib/flags.ml) by - bumping all the version numbers by one, and update the interpretations - of those flags in [`toplevel/coqargs.ml`](/toplevel/coqargs.ml) and - [`vernac/g_vernac.mlg`](/vernac/g_vernac.mlg). - + [ ] Update the files - [`test-suite/success/CompatCurrentFlag.v`](/test-suite/success/CompatCurrentFlag.v), - [`test-suite/success/CompatPreviousFlag.v`](/test-suite/success/CompatPreviousFlag.v), - and - [`test-suite/success/CompatOldFlag.v`](/test-suite/success/CompatOldFlag.v) - by bumping all version numbers by 1. - + [ ] Decide what to do about all test-suite files which mention `-compat - W.W` or `Coq.Comapt.CoqWW` (which is no longer valid, since we only - keep compatibility against the two previous versions) - [ ] Ensure that an appropriate version of the plugins we will distribute with Coq has been tagged. - [ ] Have some people test the recently auto-generated Windows and MacOS 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 $? |