CI simple-tests: separate github action job for qRHL

Separate qRHL tests in ci/simple-tests from Coq tests such that they
can run in a separate action. Before, the qRHL test was running twice,
as part of simple-tests and additionally in test-indent.

.github/workflows/test.yml

@@ -209,7 +209,7 @@ jobs:
           endGroup
 
   ###########################################################################
-  ####### Additional tests in ci/simple-tests
+  ####### Additional tests in ci/simple-tests for Coq
   ###########################################################################
   simple-tests:
     runs-on: ubuntu-latest
@@ -266,7 +266,7 @@ jobs:
           endGroup
           startGroup Run tests
             sudo chown -R coq:coq ./ci
-            make -C ci/simple-tests all
+            make -C ci/simple-tests coq-all
           endGroup
 
   ###########################################################################
@@ -299,7 +299,34 @@ jobs:
 
     - run: emacs --version
     - run: make -C ci/test-indent
-
-    # Testing this here because this job runs with all Emacs versions
-    - run: make -C ci/simple-tests test-qrhl.success
 
+  ###########################################################################
+  ####### Additional tests in ci/simple-tests for qRHL
+  ###########################################################################
+  # Run qRHL tests in ci/simple-tests on all supported emacs versions
+  # without qRHL installed.
+  test-qrhl:
+    runs-on: ubuntu-latest
+
+    strategy:
+      matrix:
+        emacs_version:
+          - 26.3
+          - 27.1
+          - 27.2
+          - 28.1
+          - 28.2
+          - 29.1
+      max-parallel: 4
+      # don't cancel all in-progress jobs if one matrix job fails:
+      fail-fast: false
+
+    steps:
+    - uses: actions/checkout@v2
+
+    - uses: purcell/setup-emacs@master
+      with:
+        version: ${{ matrix.emacs_version }}
+
+    - run: emacs --version
+    - run: make -C ci/simple-tests qrhl-all

ci/simple-tests/Makefile

@@ -8,12 +8,19 @@
 # SPDX-License-Identifier: GPL-3.0-or-later
 
 
-TESTS:=$(wildcard test-*.el)
-SUCCESS:=$(TESTS:.el=.success)
+COQ_TESTS:=$(wildcard coq-test-*.el)
+QRHL_TESTS:=$(wildcard qrhl-test-*.el)
 
-all: $(SUCCESS)
+COQ_SUCCESS:=$(COQ_TESTS:.el=.success)
+QRHL_SUCCESS:=$(QRHL_TESTS:.el=.success)
 
-test-%.success: test-%.el
+.PHONY: coq-all
+coq-all: $(COQ_SUCCESS)
+
+.PHONY: qrhl-all
+qrhl-all: $(QRHL_SUCCESS)
+
+%.success: %.el
 	emacs -batch -l ../../generic/proof-site.el -l $< \
 		-f ert-run-tests-batch-and-exit \
 	&& touch $@

ci/simple-tests/README.md

@@ -1,25 +1,29 @@
 This directory contains a number of more simple tests, that can
 all run in the same directory.
 
-# Overview of existing tests
+# Overview of existing tests for Coq
 
-test-coqtop-unavailable
+coq-test-coqtop-unavailable
 : open a file with PG when no coqtop is available
-test-omit-proofs
+coq-test-omit-proofs
 : test the omit proofs feature
-coq-par-job-needs-compilation-quick
+coq-test-par-job-needs-compilation-quick
 : test coq-par-job-needs-compilation-quick by enumerating all
   possible cases
-test-prelude-correct
+coq-test-prelude-correct
 : test that the Proof General prelude is correct
-test-qrhl
+
+# Overview of existing tests for qRHL
+
+qrhl-test-input
 : tests relating to the qRHL prover
 
 
 # Important conventions
 
-The Makefile runs all ERT tests in all `test-*.el` files.
-Therefore, the test should be written in a file matching this
-pattern.
+The Makefile runs all ERT tests in all `coq-test-*.el` and
+`qrhl-test-*.el` files for, respectively, the goals `coq-all` and
+`qrhl-all`. Therefore, new tests should be written in a file matching
+these patterns.
 
-To run all tests in a single file, do `make test-*.success`.
+To run all tests in a single file `file.el`, do `make file.success`.