Skip to content

Commit

Permalink
Merge pull request ProofGeneral#777 from hendriktews/ci-update
Browse files Browse the repository at this point in the history 
CI: update to Coq 8.19.2 and Emacs 29.4
  • Loading branch information
@hendriktews
hendriktews authored Jul 6, 2024
2 parents 99f91e8 + 5058318 commit 837f587
Show file tree
Hide file tree
Showing 7 changed files with 151 additions and 127 deletions.
110 changes: 55 additions & 55 deletions .github/workflows/test.yml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
1 change: 1 addition & 0 deletions ci/doc/.gitignore
View file
Original file line number Diff line number Diff line change
@@ -1 +1,2 @@
*.log
README.pdf
117 changes: 64 additions & 53 deletions ci/doc/README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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 `<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.
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}

Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -169,20 +175,20 @@ containers.
<!-- The content between the CIPG markers is automatically changed by
!-- the cipg program. Do not change these markers. -->
<!-- CIPG change marker: container-table -->
| | 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 |
<!-- CIPG change marker end -->

In the table above,
Expand All @@ -204,7 +210,6 @@ RC
: denotes an release candidate according to point 5.



# Testing strategy

Currently only actively supported versions are tested via GitHub
Expand Down Expand Up @@ -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.
Expand All @@ -280,32 +285,39 @@ This results in
<!-- The content between the CIPG markers is automatically changed by
!-- the cipg program. Do not change these markers. -->
<!-- CIPG change marker: testrun-number -->
33
32
<!-- CIPG change marker end -->
version pairs for the Proof General interaction tests with Coq.

<!-- The content between the CIPG markers is automatically changed by
!-- the cipg program. Do not change these markers. -->
<!-- CIPG change marker: testrun-table -->
| | 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 |
<!-- CIPG change marker end -->

See [Container build strategy](#contbuild) for an explanation of the
symbols in the table.

In summary, all Proof General testing jobs run
<!-- The content between the CIPG markers is automatically changed by
!-- the cipg program. Do not change these markers. -->
<!-- CIPG change marker: total-checks-number -->
125
<!-- CIPG change marker end -->
github checks.

# Keeping the GitHub action up-to-date

Expand Down Expand Up @@ -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`
Expand Down Expand Up @@ -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
Expand Down
Loading

0 comments on commit 837f587

Please sign in to comment.