Skip to content

Commit

Permalink
CI: prepare documentation and configuration for automatic updates
Browse files Browse the repository at this point in the history
Prepare ci/doc/README.md and .github/workflows/test.yml for automatic
updates of the tested Coq and Emacs versions.
  • Loading branch information
hendriktews committed Jan 21, 2024
1 parent 0ee1956 commit 0dbb71d
Show file tree
Hide file tree
Showing 3 changed files with 72 additions and 8 deletions.
36 changes: 36 additions & 0 deletions .github/workflows/test.yml
Original file line number Diff line number Diff line change
@@ -1,3 +1,10 @@
# See ../../ci/doc/README.{md,pdf} for documentation about continuous
# integration and testing of Proof General.
#
# The versions to be tested in between the CIPG markers are now and
# then automatically updated. Please consider this when changing this
# file.
#
name: CI

on:
Expand All @@ -20,12 +27,16 @@ jobs:
strategy:
matrix:
emacs_version:
# The content between the CIPG markers is automatically
# changed by the cipg program. Do not change these markers.
# CIPG change marker: build-emacs-versions
- 26.3
- 27.1
- 27.2
- 28.1
- 28.2
- 29.1
# CIPG change marker end
# at most 20 concurrent jobs per free account
# cf. https://help.github.com/en/actions/reference/workflow-syntax-for-github-actions#usage-limit
max-parallel: 4
Expand Down Expand Up @@ -65,8 +76,13 @@ jobs:
# I don't think we need to check with all emacs
# versions. The latest two should be enough, maybe even
# only the latest one.
#
# The content between the CIPG markers is automatically
# changed by the cipg program. Do not change these markers.
# CIPG change marker: magic-emacs-version
- 28.2
- 29.1
# CIPG change marker end
# don't cancel all in-progress jobs if one matrix job fails:
fail-fast: false

Expand All @@ -89,6 +105,9 @@ jobs:
strategy:
matrix:
coq_emacs_version:
# The content between the CIPG markers is automatically
# changed by the cipg program. Do not change these markers.
# CIPG change marker: test-coq-emacs-versions
- coq-8.11-emacs-26.3
- coq-8.11-emacs-29.1
- coq-8.12-emacs-27.1
Expand Down Expand Up @@ -122,6 +141,7 @@ jobs:
- coq-8.19-rc-emacs-28.1
- coq-8.19-rc-emacs-28.2
- coq-8.19-rc-emacs-29.1
# CIPG change marker end
# at most 20 concurrent jobs per free account
# cf. https://help.github.com/en/actions/reference/workflow-syntax-for-github-actions#usage-limit
max-parallel: 6
Expand Down Expand Up @@ -162,6 +182,9 @@ jobs:
strategy:
matrix:
coq_emacs_version:
# The content between the CIPG markers is automatically
# changed by the cipg program. Do not change these markers.
# CIPG change marker: compile-coq-emacs-versions
- coq-8.11-emacs-26.3
- coq-8.11-emacs-29.1
- coq-8.12-emacs-27.1
Expand Down Expand Up @@ -195,6 +218,7 @@ jobs:
- coq-8.19-rc-emacs-28.1
- coq-8.19-rc-emacs-28.2
- coq-8.19-rc-emacs-29.1
# CIPG change marker end
# don't cancel all in-progress jobs if one matrix job fails:
fail-fast: false
steps:
Expand Down Expand Up @@ -228,6 +252,9 @@ jobs:
strategy:
matrix:
coq_emacs_version:
# The content between the CIPG markers is automatically
# changed by the cipg program. Do not change these markers.
# CIPG change marker: simple-coq-emacs-versions
- coq-8.11-emacs-26.3
- coq-8.11-emacs-29.1
- coq-8.12-emacs-27.1
Expand Down Expand Up @@ -261,6 +288,7 @@ jobs:
- coq-8.19-rc-emacs-28.1
- coq-8.19-rc-emacs-28.2
- coq-8.19-rc-emacs-29.1
# CIPG change marker end
# don't cancel all in-progress jobs if one matrix job fails:
fail-fast: false

Expand Down Expand Up @@ -298,12 +326,16 @@ jobs:
strategy:
matrix:
emacs_version:
# The content between the CIPG markers is automatically
# changed by the cipg program. Do not change these markers.
# CIPG change marker: indent-emacs-versions
- 26.3
- 27.1
- 27.2
- 28.1
- 28.2
- 29.1
# CIPG change marker end
max-parallel: 4
# don't cancel all in-progress jobs if one matrix job fails:
fail-fast: false
Expand All @@ -329,12 +361,16 @@ jobs:
strategy:
matrix:
emacs_version:
# The content between the CIPG markers is automatically
# changed by the cipg program. Do not change these markers.
# CIPG change marker: qrhl-emacs-versions
- 26.3
- 27.1
- 27.2
- 28.1
- 28.2
- 29.1
# CIPG change marker end
max-parallel: 4
# don't cancel all in-progress jobs if one matrix job fails:
fail-fast: false
Expand Down
44 changes: 36 additions & 8 deletions ci/doc/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,11 @@ linkcolor: blue
This document describes the general strategy for testing Proof General
with GitHub actions and for building the necessary containers.

**Note:** The portions in this file between the CIPG markers (which
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.

build
Expand Down Expand Up @@ -78,9 +83,13 @@ standard support date is in the future.

Currently, the first actively supported versions are

| Coq | 8.11 |
|-------+------|
| Emacs | 26.3 |
<!-- The content between the CIPG markers is automatically changed by
!-- the cipg program. Do not change these markers. -->
<!-- CIPG change marker: coq-emacs-versions -->
| Coq | 8.11 |
|-------+-------|
| Emacs | 26.3 |
<!-- CIPG change marker end -->

The set of passively supported Coq/Emacs version pairs is work in
progress.
Expand Down Expand Up @@ -140,8 +149,17 @@ we build containers for the historic pairs of the last 6 years as
passively supported versions.


This results in 48 containers.

This results in
<!-- The content between the CIPG markers is automatically changed by
!-- the cipg program. Do not change these markers. -->
<!-- CIPG change marker: container-number -->
48
<!-- CIPG change marker end -->
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 |
|---------+------+------+------+------+------+------+------+------|
| 8.8 | H | | | | | | | |
Expand All @@ -156,6 +174,7 @@ This results in 48 containers.
| 8.17 | | | X | X | X | X | X | X |
| 8.18 | | | X | X | X | X | X | X |
| 8.19-rc | RC | RC | RC | RC | RC | RC | RC | RC |
<!-- CIPG change marker end -->

In the table above,

Expand Down Expand Up @@ -248,9 +267,17 @@ following points is true for *cv* and *ev*.
Running Proof General interaction tests with Coq for passively
supported versions is work in progress.

This results in 33 version pairs for the Proof General interaction
tests with Coq.

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
<!-- 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 |
|---------+------+------+------+------+------+------+------+------|
| 8.8 | | | | | | | | |
Expand All @@ -265,6 +292,7 @@ tests with Coq.
| 8.17 | | | X | X | | | X | SUP |
| 8.18 | | | X | X | N | N | X | X |
| 8.19-rc | RC | RC | RC | RC | RC | RC | RC | RC |
<!-- CIPG change marker end -->

See [Container build strategy](#contbuild) for an explanation of the
symbols in the table.
Expand Down
Binary file modified ci/doc/README.pdf
Binary file not shown.

0 comments on commit 0dbb71d

Please sign in to comment.