[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[nongnu] elpa/proof-general 0d2818cb26: ci/doc: document test strategy a
From: |
ELPA Syncer |
Subject: |
[nongnu] elpa/proof-general 0d2818cb26: ci/doc: document test strategy and the Coq/Emacs release table |
Date: |
Tue, 19 Dec 2023 04:00:14 -0500 (EST) |
branch: elpa/proof-general
commit 0d2818cb2644a55ba3bbfe3d55893e00ba391e51
Author: Hendrik Tews <hendrik@askra.de>
Commit: hendriktews <hendrik@askra.de>
ci/doc: document test strategy and the Coq/Emacs release table
---
ci/doc/.gitignore | 1 +
ci/doc/README.md | 368 ++++++++++++++++++++++++++++++++++++++++++
ci/doc/README.pdf | Bin 0 -> 48307 bytes
ci/doc/coq-emacs-releases.org | 60 +++++++
4 files changed, 429 insertions(+)
diff --git a/ci/doc/.gitignore b/ci/doc/.gitignore
new file mode 100644
index 0000000000..397b4a7624
--- /dev/null
+++ b/ci/doc/.gitignore
@@ -0,0 +1 @@
+*.log
diff --git a/ci/doc/README.md b/ci/doc/README.md
new file mode 100644
index 0000000000..98efd929a3
--- /dev/null
+++ b/ci/doc/README.md
@@ -0,0 +1,368 @@
+---
+title: 'Continuous integration and testing for Proof General'
+toc: true
+papersize: a4
+linkcolor: blue
+---
+
+# Introduction
+
+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 `<major>.<minor>` 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.
+
+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.
+
+
+<!--
+ !-- Local Variables:
+ !-- compile-command: "pandoc -N README.md -o README.pdf"
+ !-- End:
+ -->
diff --git a/ci/doc/README.pdf b/ci/doc/README.pdf
new file mode 100644
index 0000000000..fdc31be251
Binary files /dev/null and b/ci/doc/README.pdf differ
diff --git a/ci/doc/coq-emacs-releases.org b/ci/doc/coq-emacs-releases.org
new file mode 100644
index 0000000000..dfb167f835
--- /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 | | | |
[Prev in Thread] |
Current Thread |
[Next in Thread] |
- [nongnu] elpa/proof-general 0d2818cb26: ci/doc: document test strategy and the Coq/Emacs release table,
ELPA Syncer <=