Skip to content

Commit a75438a

Browse files
committed
ci-doc: document separate qRHL tests
Update documentation for commit 0dd686e.
1 parent 35d5efa commit a75438a

File tree

2 files changed

+22
-19
lines changed

2 files changed

+22
-19
lines changed

ci/doc/README.md

Lines changed: 22 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ linkcolor: blue
1010
This document describes the general strategy for testing Proof General
1111
with GitHub actions and for building the necessary containers.
1212

13-
The file `.github/workflows/test.yml` defines 5 jobs.
13+
The file `.github/workflows/test.yml` defines 6 jobs.
1414

1515
build
1616
: compile Proof General sources to bytecode and build documentation
@@ -26,25 +26,28 @@ compile-tests
2626
: run the auto-compilation tests in `ci/compile-tests`
2727

2828
simple-tests
29-
: run the tests in `ci/simple-tests`
29+
: run the Coq tests in `ci/simple-tests`
3030

3131
test-indent
3232
: run Coq source code indentation tests
33-
34-
The jobs build, check-doc-magic and test-indent run on different Emacs
35-
versions but they do not need Coq. They therefore use the GitHub
36-
hosted ubuntu-latest runner together with the `purcell/setup-emacs`
37-
action to install Emacs.
33+
34+
test-qrhl
35+
: run the qRHL tests in `ci/simple-tests`
36+
37+
The jobs build, check-doc-magic, test-indent and test-qrhl run on
38+
different Emacs versions but they do not need Coq. They therefore use
39+
the GitHub hosted ubuntu-latest runner together with the
40+
`purcell/setup-emacs` action to install Emacs.
3841

3942
The jobs test, compile-tests and simple-tests need Coq and Emacs in
4043
different version pairs. They therefore use the
41-
`proofgeneral/coq-emacs` containers build specifically for various
42-
Coq/Emacs version pairs for this purpose. This is achieved by
43-
installing Nix on specific containers from `coqorg/coq`, see
44-
`proofgeneral/coq-nix`, and then installing Emacs via Nix. There
45-
are GitLab and GitHub projects for building these containers in GitLab
46-
pipelines. However, currently this does not work and the containers
47-
are therefore build manually.
44+
`proofgeneral/coq-emacs` docker containers build specifically for
45+
various Coq/Emacs version pairs for this purpose. This is achieved by
46+
installing Nix on specific containers from `coqorg/coq`, see the
47+
`proofgeneral/coq-nix` docker repository, and then installing Emacs
48+
via Nix. There are GitLab and GitHub projects for building these
49+
containers in GitLab pipelines. However, currently this does not work
50+
and the containers are therefore build manually.
4851

4952
This document ignores Coq point releases (e.g., 8.13.2). For one
5053
reason we trust the Coq development team to not introduce changes in
@@ -108,7 +111,7 @@ of the following points is true for *cv* and *ev*.
108111

109112
#. The Coq version *cv* has been released within the last two years.
110113

111-
This point is motivated by the ability to reproduce Problems for
114+
This point is motivated by the ability to reproduce problems for
112115
recent Coq versions.
113116

114117
#. The pair (*cv*, *ev*) is an historic pair, in the sense that both
@@ -179,18 +182,18 @@ RC
179182
Currently only actively supported versions are tested via GitHub
180183
actions.
181184

182-
## Compilation and indentation
185+
## Compilation, indentation and qRHL
183186

184-
The tests defined for the build and test-indent jobs run for all
185-
actively supported Emacs versions.
187+
The tests defined for the build, test-indent and test-qrhl jobs run
188+
for all actively supported Emacs versions.
186189

187190
## Up-to-date documentation strings in the manuals
188191

189192
The error scenario here is that a documentation string that is
190193
magically included in the manuals has been updated without updating
191194
the manuals via `make magic`. It is therefore sufficient to run the
192195
test whether the manuals are up-to-date with only the latest two Emacs
193-
versions.
196+
major versions.
194197

195198
## Proof General interaction tests with Coq {#coq-ci}
196199

ci/doc/README.pdf

412 Bytes
Binary file not shown.

0 commit comments

Comments
 (0)