From 854f4cb255bf6befadc72c11bd2873ea29e8a5be Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Tue, 31 Oct 2023 11:40:13 +0100 Subject: [PATCH] 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 | 37 ++++++++++++++++--- ci/simple-tests/Makefile | 15 ++++++-- ci/simple-tests/README.md | 24 +++++++----- ...able.el => coq-test-coqtop-unavailable.el} | 0 ...omit-proofs.el => coq-test-omit-proofs.el} | 0 ...q-test-par-job-needs-compilation-quick.el} | 0 ...correct.el => coq-test-prelude-correct.el} | 0 .../{test-qrhl.el => qrhl-test-input.el} | 0 8 files changed, 57 insertions(+), 19 deletions(-) rename ci/simple-tests/{test-coqtop-unavailable.el => coq-test-coqtop-unavailable.el} (100%) rename ci/simple-tests/{test-omit-proofs.el => coq-test-omit-proofs.el} (100%) rename ci/simple-tests/{test-coq-par-job-needs-compilation-quick.el => coq-test-par-job-needs-compilation-quick.el} (100%) rename ci/simple-tests/{test-prelude-correct.el => coq-test-prelude-correct.el} (100%) rename ci/simple-tests/{test-qrhl.el => qrhl-test-input.el} (100%) diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 72b7fbfa7..669d89c0a 100644 --- a/.github/workflows/test.yml +++ b/.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 diff --git a/ci/simple-tests/Makefile b/ci/simple-tests/Makefile index 95e13d3b0..786ce6067 100644 --- a/ci/simple-tests/Makefile +++ b/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 $@ diff --git a/ci/simple-tests/README.md b/ci/simple-tests/README.md index 03f4183ac..06f5a654c 100644 --- a/ci/simple-tests/README.md +++ b/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`. diff --git a/ci/simple-tests/test-coqtop-unavailable.el b/ci/simple-tests/coq-test-coqtop-unavailable.el similarity index 100% rename from ci/simple-tests/test-coqtop-unavailable.el rename to ci/simple-tests/coq-test-coqtop-unavailable.el diff --git a/ci/simple-tests/test-omit-proofs.el b/ci/simple-tests/coq-test-omit-proofs.el similarity index 100% rename from ci/simple-tests/test-omit-proofs.el rename to ci/simple-tests/coq-test-omit-proofs.el diff --git a/ci/simple-tests/test-coq-par-job-needs-compilation-quick.el b/ci/simple-tests/coq-test-par-job-needs-compilation-quick.el similarity index 100% rename from ci/simple-tests/test-coq-par-job-needs-compilation-quick.el rename to ci/simple-tests/coq-test-par-job-needs-compilation-quick.el diff --git a/ci/simple-tests/test-prelude-correct.el b/ci/simple-tests/coq-test-prelude-correct.el similarity index 100% rename from ci/simple-tests/test-prelude-correct.el rename to ci/simple-tests/coq-test-prelude-correct.el diff --git a/ci/simple-tests/test-qrhl.el b/ci/simple-tests/qrhl-test-input.el similarity index 100% rename from ci/simple-tests/test-qrhl.el rename to ci/simple-tests/qrhl-test-input.el