From 156ed2d4d647a3ee55dbff44c1638ac9b34f5595 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Sat, 28 Oct 2023 15:21:08 +0200 Subject: [PATCH] ci/doc: document test strategy and the Coq/Emacs release table --- ci/doc/.gitignore | 2 + ci/doc/README.md | 367 ++++++++++++++++++++++++++++++++++ ci/doc/coq-emacs-releases.org | 60 ++++++ 3 files changed, 429 insertions(+) create mode 100644 ci/doc/.gitignore create mode 100644 ci/doc/README.md create mode 100644 ci/doc/coq-emacs-releases.org diff --git a/ci/doc/.gitignore b/ci/doc/.gitignore new file mode 100644 index 000000000..5eba6c3c7 --- /dev/null +++ b/ci/doc/.gitignore @@ -0,0 +1,2 @@ +*.pdf +*.log diff --git a/ci/doc/README.md b/ci/doc/README.md new file mode 100644 index 000000000..83a5ece69 --- /dev/null +++ b/ci/doc/README.md @@ -0,0 +1,367 @@ +--- +title: 'Continuous integration and testing for Proof General' +toc: false +papersize: a4 +--- + +This document describes the general strategy for testing Proof General +with GitHub actions and for building the necessary containers. + +The file `.github/workflows/test.yml` defines 5 jobs. + +build + : compile Proof General sources to bytecode and build documentation + +check-doc-magic: + : check that the documentation strings from the source code that are + magically included in the manuals are correct + +test + : run the tests in `ci/coq-tests.el` + +compile-tests + : run the auto-compilation tests in `ci/compile-tests` + +simple-tests + : run the tests in `ci/simple-tests` + +test-indent + : run Coq source code indentation tests + +The jobs build, check-doc-magic and test-indent run on different Emacs +versions but they do not need Coq. They therefore use the GitHub +hosted ubuntu-latest runner together with the `purcell/setup-emacs` +action to install Emacs. + +The jobs test, compile-tests and simple-tests need Coq and Emacs in +different version pairs. They therefore use the +`proofgeneral/coq-emacs` containers build specifically for various +Coq/Emacs version pairs for this purpose. This is achieved by +installing Nix on specific containers from `coqorg/coq`, see +`proofgeneral/coq-nix`, and then installing Emacs 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. + +# Generic strategy {#generic} + +Proof General distinguishes between active and passive support for +certain Coq/Emacs versions pairs. Active support means that tests for +these Coq/Emacs versions pairs run on each pull request and the pull +request should not be merged if one of these tests fails unexpectedly. +Passive support means that the developers refrain from knowingly +breaking the compatibility with passively supported version pairs. (In +the future we plan to also run tests on passively supported version +pairs.) + +The actively supported Coq/Emacs version pairs are all Coq/Emacs +version combinations starting from the oldest Coq and the oldest Emacs +version from all Debian and Ubuntu releases that are still enjoying +standard support. For Debian these are the releases whose end of live +date is in the future. For Ubuntu these are the releases whose end of +standard support date is in the future. + +Currently, the first actively supported versions are + +| Coq | 8.11 | +|-------+------| +| Emacs | 26.3 | + +The set of passively supported Coq/Emacs version pairs is work in +progress. + +In May 2023, shortly before Ubuntu 18.04 Bionic Beaver reached its end +of standard support, all Coq versions since 8.6 and all Emacs versions +since 25.2 were actively supported, resulting in 12 major Coq +versions, 9 Emacs versions and 108 version pairs. + +To keep test runtime and space for containers reasonable, we build +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 +container containing that Coq and Emacs version is built, in case one +of the following points is true for *cv* and *ev*. + +#. The Emacs version *ev* is present in an Debian or Ubuntu release + still enjoying standard support and the Coq version *cv* or an + earlier Coq version is present in the same release. + + This point is motivated by the ability to reproduce problems in a + supported Debian or Ubuntu installation in which Coq has been updated + via opam. + +#. The Coq version *cv* has been released within the last two years. + + This point is motivated by the ability to reproduce Problems for + recent Coq versions. + +#. The pair (*cv*, *ev*) is an historic pair, in the sense that both + versions were for several month the newest versions in the past. + E.g., in the second half of 2020 Coq 8.12 and Emacs 27.1 were + respectively the newest versions for about 6 month. Therefore the + pair (8.12, 27.1) is considered an historic pair. + + This point is motivated by the ability to reproduce Problems for + versions that may have been used by many people for several month + in the past. + +#. The Coq version *cv* is the newest Coq version or the Emacs version + *ev* is the newest Emacs version. + + This point is motivated by the compatibility of newest versions. + +#. The Coq version *cv* is a release candidate. + + This point is motivated by the compatibility of release candidates. + + +Eventually we will also spell out the container build strategy for the +passively supported versions. For now, in addition to the rules above, +we build containers for the historic pairs of the last 6 years as +passively supported versions. + + +This results in 43 containers. + +| | 25.3 | 26.1 | 26.2 | 26.3 | 27.1 | 27.2 | 28.1 | 28.2 | 29.1 | +|---------+------+------+------+------+------+------+------+------+------| +| 8.7 | H | | | | | | | | | +| 8.8 | | H | | | | | | | | +| 8.9 | | | H | | | | | | | +| 8.10 | | | | H | | | | | | +| 8.11 | | | | SUP | | | | | N | +| 8.12 | | | | SUP | SUP | | | | N | +| 8.13 | | | | SUP | SUP | H | | | N | +| 8.14 | | | | X | X | X | X | X | X | +| 8.15 | | | | X | X | X | X | X | X | +| 8.16 | | | | X | X | X | X | X | X | +| 8.17 | | | | X | X | X | X | X | X | +| 8.18 | | | | X | X | X | X | X | X | + +In the table above, + +SUP + : denotes a supported pair according to point 1. above. + +X + : denotes a Coq release within the last 2 years according to point 2. + above. + +H + : denotes an historic pair according to point 3. + +N + : denotes newest Coq or Emacs versions according to point 4. + +RC + : denotes an release candidate according to point 5. + + + +# Testing strategy + +Currently only actively supported versions are tested via GitHub +actions. + +## Compilation and indentation + +The tests defined for the build and test-indent jobs run for all +actively supported Emacs versions. + +## Up-to-date documentation strings in the manuals + +The error scenario here is that a documentation string that is +magically included in the manuals has been updated without updating +the manuals via `make magic`. It is therefore sufficient to run the +test whether the manuals are up-to-date with only the latest two Emacs +versions. + +## Proof General interaction tests with Coq {#coq-ci} + +The tests for the GitHub actions test, compile-tests and simple-tests +can obviously only run for those version pairs for which containers +have been build, see [Container build strategy](#contbuild). To limit +the required resources, the tests only run on a subset of the +available containers. + +The jobs test, compile-tests and simple-tests run for an actively +supported Coq/Emacs version pair (*cv*, *ev*), in case one of the +following points is true for *cv* and *ev*. + +#. The version pair (*cv*, *ev*) is present in an Debian or Ubuntu release + still enjoying standard support. + + This point is for Proof General users using one of these currently + supported releases. + +#. The Emacs version *ev* is present in an Debian or Ubuntu release + still enjoying standard support and the Coq version *ev* has been + released in the last 18 month and is either equal or greater than + the Coq version of this Debian or Ubuntu release. + + This point is for Proof General users that use one of the supported + 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. + +#. The pair (*cv*, *ev*) is an historic pair in the same sense as + above. + + This point is motivated by the compatibility with version pairs + that may have enjoyed some wider use. + +#. The Coq version *cv* is the newest Coq version or the Emacs version + *ev* is the newest Emacs version. + + This point is motivated by the compatibility of newest versions. + +#. The Coq version *cv* is a release candidate. + + This point is motivated by the compatibility of release candidates. + +Running Proof General interaction tests with Coq for passively +supported versions is work in progress. + +\clearpage + +This results in 26 version pairs for the Proof General interaction +tests with Coq. + +| | 25.3 | 26.1 | 26.2 | 26.3 | 27.1 | 27.2 | 28.1 | 28.2 | 29.1 | +|---------+------+------+------+------+------+------+------+------+------| +| 8.7 | | | | | | | | | | +| 8.8 | | | | | | | | | | +| 8.9 | | | | | | | | | | +| 8.10 | | | | | | | | | | +| 8.11 | | | | SUP | | | | | N | +| 8.12 | | | | | SUP | | | | N | +| 8.13 | | | | | | H | | | N | +| 8.14 | | | | | | H | | | N | +| 8.15 | | | | X | X | | H | | N | +| 8.16 | | | | X | X | | | SUP | N | +| 8.17 | | | | X | X | | | X | SUP | +| 8.18 | | | | X | X | N | N | X | X | + +See [Container build strategy](#contbuild) for an explanation of the +symbols in the table. + + +# Keeping the GitHub action up-to-date + +Obviously, after each Coq or Emacs release and additionally every few +month the rules in the preceding sections for building containers and +for testing must be re-evaluated and the workflow file +`.github/workflows/test.yml` must be updated. + +Large portions of this process have been automated. Coq, Emacs, Debian +and Ubuntu releases must be manually added into an Org mode table in +file `coq-emacs-releases.org`. This table is read by the OCaml program +`cipg` that performs the following tasks. + +- It evaluates the rules spelled out above and generates the tables in + the Sections [Generic strategy](#generic), [Container build + strategy](#contbuild), and [Proof General interaction tests with + Coq](#coq-ci) in this document. +- It determines missing docker images and generates command lines for + building them. +- It determines superfluous docker images and deletes them. +- It generates the lines that are needed to update + `.github/workflows/test.yml`. + + +## Release table + +The release table is the Org mode table in file +`coq-emacs-releases.org`. It contains all the data that is needed to +evaluate the rules for building containers and for testing in the +preceding sections. In particular, it contains + +- Coq, Emacs, Debian and Ubuntu releases with their release date. +- The end of standard support for Debian and Ubuntu releases. +- The Coq and Emacs versions contained in these Debian and Ubuntu + releases. +- The historic pairs. + +The remainder of this section explains how to maintain this table such +that `cipg` can process it. + +#. Whenever a new version of Coq, Emacs, Debian or Ubuntu is released, + a line needs to be added manually to the release table. + +#. The date must be present in every line in the form YYYY/MM. + +#. There are 3 kinds of lines in the table. + + Coq releases + : are specified with a date and a Coq version. + + Emacs releases + : are specified with a date and an Emacs version. + + Debian or Ubuntu releases + : are specified with a date, a distribution name and an EOL date. + +#. The Coq and Emacs versions of an Debian or Ubuntu release may be + omitted. If they are not present, they are taken from the last + preceding line containing the respective version (the table is + processed from bottom to top). E.g., the line specifying the + release of Ubuntu 20.4 (on 2020/04) inherits Coq version 8.11.0 + from the preceding line and Emacs version 26.3 from 5 lines below. + +#. The lines do not need to be sorted by date. I find it clearer to + insert Debian and Ubuntu releases at a place where they can inherit + the Coq and maybe the Emacs version from a previous line, such that + these version numbers can be omitted. E.g., the line for Debian 11 + Bullseye released in 2021/08 appears before the Coq release 8.12.1 + in 2020/11, because Bullseye was released with 8.12.0. + + Sometimes it is impossible to move a Debian or Ubuntu release line + to a place where it can inherit both, the Coq and Emacs version, + without scrambling the table too much. E.g., Ubuntu 22 was released + with Coq 8.15.0 and Emacs 27.1. In this case I prefer to keep the + table sorted by Coq releases, to specify the Emacs version for + Ubuntu 22, and move the line to a place where it can inherit the Coq + version. The Emacs column therefore contains some discontinuities + (together with the date column). + +#. Historical pairs must be manually marked in column `historic`. They + are mainly used to manually select some additional version pairs + for testing and to have some sort of diagonal in the version matrix + for Proof General interaction tests. + +#. The EOL date of Debian or Ubuntu releases must also be in the form + 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. + + + diff --git a/ci/doc/coq-emacs-releases.org b/ci/doc/coq-emacs-releases.org new file mode 100644 index 000000000..dfb167f83 --- /dev/null +++ b/ci/doc/coq-emacs-releases.org @@ -0,0 +1,60 @@ +* Coq, Emacs, Debian and Ubuntu releases + This table must be maintained manually. Its content is processed + automatically, therefore please observe the requirements in Section + "Release table" in file README.md! + +| date | coq | emacs | distribution name | EOL | historic | +|---------+--------+-------+-------------------+----------+----------| +| 2023/09 | 8.18.0 | | | | | +| 2023/07 | | 29.1 | | | | +| 2023/06 | 8.17.1 | | | | | +| 2023/10 | | 29.1 | ubu 23 mantic mi | 2024/07 | | +| 2023/03 | 8.17.0 | | | | | +| 2023/06 | | | deb 12 bookworm | 2026/06? | | +| 2023/04 | | | ubu 23 lun lobs | 2024/01 | | +| 2022/11 | 8.16.1 | | | | X | +| 2022/09 | 8.16.0 | 28.2 | | | | +| 2022/05 | 8.15.2 | | | | | +| 2022/04 | | 28.1 | | | X | +| 2022/03 | 8.15.1 | | | | | +| 2022/04 | | 27.1 | ubu 22 jammy jel | 2027/04 | | +| 2022/01 | 8.15.0 | | | | | +| 2021/12 | 8.14.1 | | | | X | +| 2021/10 | 8.14.0 | | | | | +| 2021/04 | 8.13.2 | | | | X | +| 2021/03 | | 27.2 | | | | +| 2021/02 | 8.13.1 | | | | | +| 2021/01 | 8.13.0 | | | | | +| 2020/12 | 8.12.2 | | | | X | +| 2020/11 | 8.12.1 | | | | | +| 2021/10 | | | ubu 21 impish | 2022/07 | | +| 2021/08 | | | deb 11 bullseye | 2024/07? | | +| 2020/08 | | 27.1 | | | | +| 2020/07 | 8.12.0 | | | | | +| 2020/06 | 8.11.2 | | | | | +| 2020/04 | 8.11.1 | | | | X | +| 2020/04 | | | ubu 20.4 focal | 2025/04 | | +| 2020/01 | 8.11.0 | | | | | +| 2019/11 | 8.10.2 | | | | | +| 2019/10 | 8.10.1 | | | | X | +| 2019/10 | 8.10.0 | | | | | +| 2019/08 | | 26.3 | | | | +| 2019/05 | 8.9.1 | | | | X | +| 2019/07 | | | deb 10 buster | 2022/09 | | +| 2019/04 | | 26.2 | | | | +| 2019/01 | 8.9.0 | | | | | +| 2018/09 | 8.8.2 | | | | X | +| 2018/07 | 8.8.1 | | | | | +| 2018/05 | | 26.1 | | | | +| 2018/04 | 8.8.0 | | | | | +| 2018/02 | 8.7.2 | | | | | +| 2017/12 | 8.7.1 | | | | X | +| 2017/10 | 8.7.0 | | | | | +| 2017/09 | | 25.3 | | | | +| 2017/07 | 8.6.1 | | | | X | +| 2018/04 | | | ubu 18.04 bionic | 2023/04 | | +| 2017/04 | | 25.2 | | | | +| 2017/06 | | | deb 9 stretch | 2020/06 | | +| 2016/12 | 8.6 | | | | | +| 2016/10 | 8.5pl3 | | | | | +| 2016/09 | | 25.1 | | | |