diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index c81ed67bc..f14783b45 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -38,6 +38,7 @@ jobs: - 29.1 - 29.2 - 29.3 + - 29.4 # CIPG change marker end # don't cancel all in-progress jobs if one matrix job fails: fail-fast: false @@ -80,7 +81,7 @@ jobs: # changed by the cipg program. Do not change these markers. # CIPG change marker: magic-emacs-version - 28.2 - - 29.3 + - 29.4 # CIPG change marker end # don't cancel all in-progress jobs if one matrix job fails: fail-fast: false @@ -108,38 +109,37 @@ jobs: # changed by the cipg program. Do not change these markers. # CIPG change marker: test-coq-emacs-versions - coq-8.11.2-emacs-26.3 - - coq-8.11.2-emacs-29.3 + - coq-8.11.2-emacs-29.4 - coq-8.12.2-emacs-27.1 - - coq-8.12.2-emacs-29.3 + - coq-8.12.2-emacs-29.4 - coq-8.13.2-emacs-27.2 - - coq-8.13.2-emacs-29.3 + - coq-8.13.2-emacs-29.4 - coq-8.14.1-emacs-27.2 - - coq-8.14.1-emacs-29.3 + - coq-8.14.1-emacs-29.4 - coq-8.15.2-emacs-27.1 - coq-8.15.2-emacs-28.1 - - coq-8.15.2-emacs-29.3 - - coq-8.16.1-emacs-26.3 - - coq-8.16.1-emacs-27.1 + - coq-8.15.2-emacs-29.4 - coq-8.16.1-emacs-28.2 - - coq-8.16.1-emacs-29.3 + - coq-8.16.1-emacs-29.4 - coq-8.17.1-emacs-26.3 - coq-8.17.1-emacs-27.1 - coq-8.17.1-emacs-28.2 - coq-8.17.1-emacs-29.1 - - coq-8.17.1-emacs-29.3 + - coq-8.17.1-emacs-29.4 - coq-8.18.0-emacs-26.3 - coq-8.18.0-emacs-27.1 - coq-8.18.0-emacs-28.2 - coq-8.18.0-emacs-29.1 - - coq-8.18.0-emacs-29.3 - - coq-8.19.1-emacs-26.3 - - coq-8.19.1-emacs-27.1 - - coq-8.19.1-emacs-27.2 - - coq-8.19.1-emacs-28.1 - - coq-8.19.1-emacs-28.2 - - coq-8.19.1-emacs-29.1 - - coq-8.19.1-emacs-29.2 - - coq-8.19.1-emacs-29.3 + - coq-8.18.0-emacs-29.4 + - coq-8.19.2-emacs-26.3 + - coq-8.19.2-emacs-27.1 + - coq-8.19.2-emacs-27.2 + - coq-8.19.2-emacs-28.1 + - coq-8.19.2-emacs-28.2 + - coq-8.19.2-emacs-29.1 + - coq-8.19.2-emacs-29.2 + - coq-8.19.2-emacs-29.3 + - coq-8.19.2-emacs-29.4 # CIPG change marker end # don't cancel all in-progress jobs if one matrix job fails: fail-fast: false @@ -182,38 +182,37 @@ jobs: # changed by the cipg program. Do not change these markers. # CIPG change marker: compile-coq-emacs-versions - coq-8.11.2-emacs-26.3 - - coq-8.11.2-emacs-29.3 + - coq-8.11.2-emacs-29.4 - coq-8.12.2-emacs-27.1 - - coq-8.12.2-emacs-29.3 + - coq-8.12.2-emacs-29.4 - coq-8.13.2-emacs-27.2 - - coq-8.13.2-emacs-29.3 + - coq-8.13.2-emacs-29.4 - coq-8.14.1-emacs-27.2 - - coq-8.14.1-emacs-29.3 + - coq-8.14.1-emacs-29.4 - coq-8.15.2-emacs-27.1 - coq-8.15.2-emacs-28.1 - - coq-8.15.2-emacs-29.3 - - coq-8.16.1-emacs-26.3 - - coq-8.16.1-emacs-27.1 + - coq-8.15.2-emacs-29.4 - coq-8.16.1-emacs-28.2 - - coq-8.16.1-emacs-29.3 + - coq-8.16.1-emacs-29.4 - coq-8.17.1-emacs-26.3 - coq-8.17.1-emacs-27.1 - coq-8.17.1-emacs-28.2 - coq-8.17.1-emacs-29.1 - - coq-8.17.1-emacs-29.3 + - coq-8.17.1-emacs-29.4 - coq-8.18.0-emacs-26.3 - coq-8.18.0-emacs-27.1 - coq-8.18.0-emacs-28.2 - coq-8.18.0-emacs-29.1 - - coq-8.18.0-emacs-29.3 - - coq-8.19.1-emacs-26.3 - - coq-8.19.1-emacs-27.1 - - coq-8.19.1-emacs-27.2 - - coq-8.19.1-emacs-28.1 - - coq-8.19.1-emacs-28.2 - - coq-8.19.1-emacs-29.1 - - coq-8.19.1-emacs-29.2 - - coq-8.19.1-emacs-29.3 + - coq-8.18.0-emacs-29.4 + - coq-8.19.2-emacs-26.3 + - coq-8.19.2-emacs-27.1 + - coq-8.19.2-emacs-27.2 + - coq-8.19.2-emacs-28.1 + - coq-8.19.2-emacs-28.2 + - coq-8.19.2-emacs-29.1 + - coq-8.19.2-emacs-29.2 + - coq-8.19.2-emacs-29.3 + - coq-8.19.2-emacs-29.4 # CIPG change marker end # don't cancel all in-progress jobs if one matrix job fails: fail-fast: false @@ -252,38 +251,37 @@ jobs: # changed by the cipg program. Do not change these markers. # CIPG change marker: simple-coq-emacs-versions - coq-8.11.2-emacs-26.3 - - coq-8.11.2-emacs-29.3 + - coq-8.11.2-emacs-29.4 - coq-8.12.2-emacs-27.1 - - coq-8.12.2-emacs-29.3 + - coq-8.12.2-emacs-29.4 - coq-8.13.2-emacs-27.2 - - coq-8.13.2-emacs-29.3 + - coq-8.13.2-emacs-29.4 - coq-8.14.1-emacs-27.2 - - coq-8.14.1-emacs-29.3 + - coq-8.14.1-emacs-29.4 - coq-8.15.2-emacs-27.1 - coq-8.15.2-emacs-28.1 - - coq-8.15.2-emacs-29.3 - - coq-8.16.1-emacs-26.3 - - coq-8.16.1-emacs-27.1 + - coq-8.15.2-emacs-29.4 - coq-8.16.1-emacs-28.2 - - coq-8.16.1-emacs-29.3 + - coq-8.16.1-emacs-29.4 - coq-8.17.1-emacs-26.3 - coq-8.17.1-emacs-27.1 - coq-8.17.1-emacs-28.2 - coq-8.17.1-emacs-29.1 - - coq-8.17.1-emacs-29.3 + - coq-8.17.1-emacs-29.4 - coq-8.18.0-emacs-26.3 - coq-8.18.0-emacs-27.1 - coq-8.18.0-emacs-28.2 - coq-8.18.0-emacs-29.1 - - coq-8.18.0-emacs-29.3 - - coq-8.19.1-emacs-26.3 - - coq-8.19.1-emacs-27.1 - - coq-8.19.1-emacs-27.2 - - coq-8.19.1-emacs-28.1 - - coq-8.19.1-emacs-28.2 - - coq-8.19.1-emacs-29.1 - - coq-8.19.1-emacs-29.2 - - coq-8.19.1-emacs-29.3 + - coq-8.18.0-emacs-29.4 + - coq-8.19.2-emacs-26.3 + - coq-8.19.2-emacs-27.1 + - coq-8.19.2-emacs-27.2 + - coq-8.19.2-emacs-28.1 + - coq-8.19.2-emacs-28.2 + - coq-8.19.2-emacs-29.1 + - coq-8.19.2-emacs-29.2 + - coq-8.19.2-emacs-29.3 + - coq-8.19.2-emacs-29.4 # CIPG change marker end # don't cancel all in-progress jobs if one matrix job fails: fail-fast: false @@ -333,6 +331,7 @@ jobs: - 29.1 - 29.2 - 29.3 + - 29.4 # CIPG change marker end # don't cancel all in-progress jobs if one matrix job fails: fail-fast: false @@ -369,6 +368,7 @@ jobs: - 29.1 - 29.2 - 29.3 + - 29.4 # CIPG change marker end # don't cancel all in-progress jobs if one matrix job fails: fail-fast: false diff --git a/ci/doc/.gitignore b/ci/doc/.gitignore index 397b4a762..0602fd77a 100644 --- a/ci/doc/.gitignore +++ b/ci/doc/.gitignore @@ -1 +1,2 @@ *.log +README.pdf diff --git a/ci/doc/README.md b/ci/doc/README.md index 3ab4714cb..4ebedd8ba 100644 --- a/ci/doc/README.md +++ b/ci/doc/README.md @@ -24,7 +24,7 @@ are invisible in the PDF version) are now and then automatically updated by the `cipg` program. Please consider this when changing this file. -The file `.github/workflows/test.yml` defines 6 jobs. +The file `.github/workflows/test.yml` defines 7 jobs. build : compile Proof General sources to bytecode and build documentation @@ -63,14 +63,19 @@ via Nix. There are GitLab and GitHub projects for building these containers in GitLab pipelines. However, currently this does not work and the containers are therefore build manually. -This document ignores Coq point releases (e.g., 8.13.2). For one -reason we trust the Coq development team to not introduce changes in -point releases that Proof General should care about. Another reason is -that the `coqorg/coq` docker images are only available for the latest -point release of any minor version. Therefore, in this document, a Coq -version number `.` always stands for the latest point -release of that minor release. E.g., 8.17 stands for 8.17.1 released -in 2023/06. +Coq minor releases (e.g., 8.19.0) are often followed by bug fix +releases (e.g., 8.19.1 and 8.19.2). For testing Proof General we only +use the latest bug fix release of certain Coq releases (e.g., we do +test 8.19.2 but neither 8.19.0 nor 8.19.1). One reason is that testing +original minor releases (e.g., 8.19.0) or outdated bug fix releases +(e.g., 8.19.1) does not make much sense. Another reason is that +`coqorg/coq` does only provide containers for the latest bug fix +release of each minor release. Admittedly, the effects of only testing +the latest bug fix release are not always optimal. For instance, in +2024, Coq 8.11 is tested, because Ubuntu 20.04 Focal Fossa was +released with Coq 8.11.0, however, Proof General testing uses Coq +8.11.2. + # Generic strategy {#generic} @@ -113,6 +118,7 @@ containers only for a subset of the actively supported version pairs and only a subset of these containers are used by the GitHub action jobs. + # Container build strategy {#contbuild} For an actively supported Coq/Emacs version pair (*cv*, *ev*), a @@ -169,20 +175,20 @@ containers. -| | 26.1 | 26.2 | 26.3 | 27.1 | 27.2 | 28.1 | 28.2 | 29.1 | 29.2 | 29.3 | -|---------+------+------+------+------+------+------+------+------+------+------| -| 8.8.2 | H | | | | | | | | | | -| 8.9.1 | | H | | | | | | | | | -| 8.10.2 | | | H | | | | | | | | -| 8.11.2 | | | SUP | | | | | | | N | -| 8.12.2 | | | SUP | SUP | | | | | | N | -| 8.13.2 | | | SUP | SUP | H | | | | | N | -| 8.14.1 | | | SUP | SUP | H | | | | | N | -| 8.15.2 | | | X | X | X | X | X | X | X | X | -| 8.16.1 | | | X | X | X | X | X | X | X | X | -| 8.17.1 | | | X | X | X | X | X | X | X | X | -| 8.18.0 | | | X | X | X | X | X | X | X | X | -| 8.19.1 | | | X | X | X | X | X | X | X | X | +| | 26.1 | 26.2 | 26.3 | 27.1 | 27.2 | 28.1 | 28.2 | 29.1 | 29.2 | 29.3 | 29.4 | +|---------+------+------+------+------+------+------+------+------+------+------+------| +| 8.8.2 | H | | | | | | | | | | | +| 8.9.1 | | H | | | | | | | | | | +| 8.10.2 | | | H | | | | | | | | | +| 8.11.2 | | | SUP | | | | | | | | N | +| 8.12.2 | | | SUP | SUP | | | | | | | N | +| 8.13.2 | | | SUP | SUP | H | | | | | | N | +| 8.14.1 | | | SUP | SUP | H | | | | | | N | +| 8.15.2 | | | SUP | SUP | | H | | | | | N | +| 8.16.1 | | | X | X | X | X | X | X | X | X | X | +| 8.17.1 | | | X | X | X | X | X | X | X | X | X | +| 8.18.0 | | | X | X | X | X | X | X | X | X | X | +| 8.19.2 | | | X | X | X | X | X | X | X | X | X | In the table above, @@ -204,7 +210,6 @@ RC : denotes an release candidate according to point 5. - # Testing strategy Currently only actively supported versions are tested via GitHub @@ -250,13 +255,13 @@ following points is true for *cv* and *ev*. Debian or Ubuntu versions and now and then upgrade their Coq version via opam. - For example, in October 2023 the 18 month limit includes Coq 8.15 - (last minor version released in 2022/05) but excludes 8.14 (last - minor version released in 2021/12). Therefore we do test the pair - (8.15, 27.1) but we don't test (8.14, 27.1). We neither test (8.15, - 27.2), because there is no Debian or Ubuntu release containing - 27.2. Further, we don't test (8.15, 28.2), because Ubuntu 23 and - Debian 12, which both contain Emacs 28.2, contain Coq 8.16. + For example, in October 2023 the 18 month limit includes Coq 8.15.2 + (released in 2022/05) but excludes 8.14.1 (last minor 8.14 version, + released in 2021/12). Therefore we do test the pair (8.15.2, 27.1) + but we don't test (8.14.1, 27.1). We neither test (8.15.2, 27.2), + because there is no Debian or Ubuntu release containing 27.2. + Further, we don't test (8.15.2, 28.2), because Ubuntu 23 and Debian + 12, which both contain Emacs 28.2, contain Coq 8.16. #. The pair (*cv*, *ev*) is an historic pair in the same sense as above. @@ -280,32 +285,39 @@ This results in -33 +32 version pairs for the Proof General interaction tests with Coq. -| | 26.1 | 26.2 | 26.3 | 27.1 | 27.2 | 28.1 | 28.2 | 29.1 | 29.2 | 29.3 | -|---------+------+------+------+------+------+------+------+------+------+------| -| 8.8.2 | | | | | | | | | | | -| 8.9.1 | | | | | | | | | | | -| 8.10.2 | | | | | | | | | | | -| 8.11.2 | | | SUP | | | | | | | N | -| 8.12.2 | | | | SUP | | | | | | N | -| 8.13.2 | | | | | H | | | | | N | -| 8.14.1 | | | | | H | | | | | N | -| 8.15.2 | | | | SUP | | H | | | | N | -| 8.16.1 | | | X | X | | | X | | | N | -| 8.17.1 | | | X | X | | | X | SUP | | N | -| 8.18.0 | | | X | X | | | X | X | | N | -| 8.19.1 | | | X | X | N | N | X | X | N | N | +| | 26.1 | 26.2 | 26.3 | 27.1 | 27.2 | 28.1 | 28.2 | 29.1 | 29.2 | 29.3 | 29.4 | +|---------+------+------+------+------+------+------+------+------+------+------+------| +| 8.8.2 | | | | | | | | | | | | +| 8.9.1 | | | | | | | | | | | | +| 8.10.2 | | | | | | | | | | | | +| 8.11.2 | | | SUP | | | | | | | | N | +| 8.12.2 | | | | SUP | | | | | | | N | +| 8.13.2 | | | | | H | | | | | | N | +| 8.14.1 | | | | | H | | | | | | N | +| 8.15.2 | | | | SUP | | H | | | | | N | +| 8.16.1 | | | | | | | SUP | | | | N | +| 8.17.1 | | | X | X | | | X | X | | | N | +| 8.18.0 | | | X | X | | | X | X | | | N | +| 8.19.2 | | | X | X | N | N | X | X | N | N | N | See [Container build strategy](#contbuild) for an explanation of the symbols in the table. +In summary, all Proof General testing jobs run + + +125 + +github checks. # Keeping the GitHub action up-to-date @@ -396,11 +408,10 @@ that `cipg` can process it. YYYY/MM. Trailing non-digit characters are ignored. I use `?` to indicate EOL dates that have not yet been fixed. -#. In Coq version numbers the patch level is ignored. Versions of - release candidates must be of the form `8.10rc` or `8.10-rc`. - `cipg` is not able to recognize outdated release candidates. The - release candidate must therefore be deleted when the release - happens. +#. Versions of release candidates must be of the form `8.10rc` or + `8.10-rc`. `cipg` is not able to recognize outdated release + candidates. The release candidate must therefore be deleted when + the release happens. ## `cipg` @@ -461,12 +472,12 @@ below. The options described in this subsection perform destructive updates or removals. Use them with care. -The option `ci-change` updates `README.md` (this file) and `test.yml` +The option `-ci-change` updates `README.md` (this file) and `test.yml` in the Proof-General repository identified by `cipg` with the new configuration. See option `-pg-repo` to change the Proof General repository. The updates are done in place, without taking backups, which is not a problem, if there are no unstaged changes. In -particular, the option `ci-change` changes +particular, the option `-ci-change` changes - the three tables in the Sections [Generic strategy](#generic), [Container build strategy](#contbuild), and [Proof General diff --git a/ci/doc/coq-emacs-releases.org b/ci/doc/coq-emacs-releases.org index 7df3911fc..ef67aba1d 100644 --- a/ci/doc/coq-emacs-releases.org +++ b/ci/doc/coq-emacs-releases.org @@ -13,10 +13,11 @@ | date | coq | emacs | distribution name | EOL | historic | |---------+--------+-------+-------------------+----------+----------| +| 2024/06 | 8.19.2 | 29.4 | | | | | 2024/03 | 8.19.1 | 29.3 | | | | | 2024/01 | 8.19.0 | 29.2 | | | | | 2023/09 | 8.18.0 | | | | | -| 2023/07 | | 29.1 | | | | +| 2023/07 | | 29.1 | | | X | | 2023/06 | 8.17.1 | | | | | | 2023/10 | | 29.1 | ubu 23 mantic mi | 2024/07 | | | 2023/03 | 8.17.0 | | | | | diff --git a/ci/doc/currently-used-coq-emacs-versions b/ci/doc/currently-used-coq-emacs-versions index 8f9b1c0cd..2ccedee92 100644 --- a/ci/doc/currently-used-coq-emacs-versions +++ b/ci/doc/currently-used-coq-emacs-versions @@ -2,26 +2,22 @@ coq-8.8.2-emacs-26.1 coq-8.9.1-emacs-26.2 coq-8.10.2-emacs-26.3 coq-8.11.2-emacs-26.3 -coq-8.11.2-emacs-29.3 +coq-8.11.2-emacs-29.4 coq-8.12.2-emacs-26.3 coq-8.12.2-emacs-27.1 -coq-8.12.2-emacs-29.3 +coq-8.12.2-emacs-29.4 coq-8.13.2-emacs-26.3 coq-8.13.2-emacs-27.1 coq-8.13.2-emacs-27.2 -coq-8.13.2-emacs-29.3 +coq-8.13.2-emacs-29.4 coq-8.14.1-emacs-26.3 coq-8.14.1-emacs-27.1 coq-8.14.1-emacs-27.2 -coq-8.14.1-emacs-29.3 +coq-8.14.1-emacs-29.4 coq-8.15.2-emacs-26.3 coq-8.15.2-emacs-27.1 -coq-8.15.2-emacs-27.2 coq-8.15.2-emacs-28.1 -coq-8.15.2-emacs-28.2 -coq-8.15.2-emacs-29.1 -coq-8.15.2-emacs-29.2 -coq-8.15.2-emacs-29.3 +coq-8.15.2-emacs-29.4 coq-8.16.1-emacs-26.3 coq-8.16.1-emacs-27.1 coq-8.16.1-emacs-27.2 @@ -30,6 +26,7 @@ coq-8.16.1-emacs-28.2 coq-8.16.1-emacs-29.1 coq-8.16.1-emacs-29.2 coq-8.16.1-emacs-29.3 +coq-8.16.1-emacs-29.4 coq-8.17.1-emacs-26.3 coq-8.17.1-emacs-27.1 coq-8.17.1-emacs-27.2 @@ -38,6 +35,7 @@ coq-8.17.1-emacs-28.2 coq-8.17.1-emacs-29.1 coq-8.17.1-emacs-29.2 coq-8.17.1-emacs-29.3 +coq-8.17.1-emacs-29.4 coq-8.18.0-emacs-26.3 coq-8.18.0-emacs-27.1 coq-8.18.0-emacs-27.2 @@ -46,11 +44,13 @@ coq-8.18.0-emacs-28.2 coq-8.18.0-emacs-29.1 coq-8.18.0-emacs-29.2 coq-8.18.0-emacs-29.3 -coq-8.19.1-emacs-26.3 -coq-8.19.1-emacs-27.1 -coq-8.19.1-emacs-27.2 -coq-8.19.1-emacs-28.1 -coq-8.19.1-emacs-28.2 -coq-8.19.1-emacs-29.1 -coq-8.19.1-emacs-29.2 -coq-8.19.1-emacs-29.3 +coq-8.18.0-emacs-29.4 +coq-8.19.2-emacs-26.3 +coq-8.19.2-emacs-27.1 +coq-8.19.2-emacs-27.2 +coq-8.19.2-emacs-28.1 +coq-8.19.2-emacs-28.2 +coq-8.19.2-emacs-29.1 +coq-8.19.2-emacs-29.2 +coq-8.19.2-emacs-29.3 +coq-8.19.2-emacs-29.4 diff --git a/ci/doc/currently-used-coq-nix-versions b/ci/doc/currently-used-coq-nix-versions index b61d15b60..e68fb6356 100644 --- a/ci/doc/currently-used-coq-nix-versions +++ b/ci/doc/currently-used-coq-nix-versions @@ -9,4 +9,4 @@ 8.16.1 8.17.1 8.18.0 -8.19.1 +8.19.2 diff --git a/ci/tools/cipg.ml b/ci/tools/cipg.ml index 0d719c64f..160f14278 100644 --- a/ci/tools/cipg.ml +++ b/ci/tools/cipg.ml @@ -1570,6 +1570,15 @@ let main() = print_matrix "CI pairs" coqs emacses ci_pairs; print_endline ""; check_matrix_subset coqs emacses ci_pairs conts; + let total_test_runs = + 3 * (count_filled_matrix_cells ci_pairs) + + 3 * ((snd (list_last emacses)) (* index of last emacs version *) + - (* indes of first emacs version *) + (get_version_index first_active_emacs emacses) + + 1) + + 2 (* doc magic *) + in + Printf.printf "\n%d github checks in total\n" total_test_runs; if !do_containers then begin print_endline "\n\nCHECK MISSING AND SUPERFLUOUS CONTAINERS\n"; @@ -1618,6 +1627,8 @@ let main() = (count_filled_matrix_cells ci_pairs)); md_file_change_wrapper readme_file "testrun-table" (output_matrix coqs emacses ci_pairs); + md_file_change_wrapper readme_file "total-checks-number" + (fun oc -> Printf.fprintf oc "%d\n" total_test_runs); (* In test.yml update the version numbers for all test jobs. *) List.iter