CI simple-tests: separate github action job for qRHL #527
Workflow file for this run
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: CI | |
| on: | |
| push: | |
| branches: | |
| #- master | |
| #- hybrid | |
| - "**" | |
| pull_request: | |
| branches: | |
| - '**' | |
| jobs: | |
| ########################################################################### | |
| ####### compile and build manual | |
| ########################################################################### | |
| build: | |
| runs-on: ubuntu-latest | |
| strategy: | |
| matrix: | |
| emacs_version: | |
| - 26.3 | |
| - 27.1 | |
| - 27.2 | |
| - 28.1 | |
| - 28.2 | |
| - 29.1 | |
| # 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 | |
| # 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 | |
| # Erik: Extend this with linting? | |
| - name: Install makeinfo | |
| run: sudo apt-get update -y -q && sudo DEBIAN_FRONTEND=noninteractive apt-get install -y -q --no-install-recommends texinfo | |
| - run: make doc.info | |
| ########################################################################### | |
| ####### make magic | |
| ########################################################################### | |
| # Check that the texinfo sources of the manual can be updated | |
| # with the documentation strings for variables and functions in | |
| # the source code and that the manual is actually up-to-date. | |
| # If the final git diff fails, then somebody forgot to update | |
| # the manuals with ``make -C doc magic'' after changing a | |
| # variable or function documentation that appears in one of the | |
| # manuals. | |
| check-doc-magic: | |
| runs-on: ubuntu-latest | |
| strategy: | |
| matrix: | |
| emacs_version: | |
| # I don't think we need to check with all emacs | |
| # versions. The latest two should be enough, maybe even | |
| # only the latest one. | |
| - 28.2 | |
| - 29.1 | |
| # 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 doc magic | |
| - run: git diff --exit-code -- doc | |
| ########################################################################### | |
| ####### first tests: ci/test.sh runs tests in ci/coq-tests.el | |
| ########################################################################### | |
| test: | |
| runs-on: ubuntu-latest | |
| strategy: | |
| matrix: | |
| coq_emacs_version: | |
| - coq-8.11-emacs-26.3 | |
| - coq-8.11-emacs-29.1 | |
| - coq-8.12-emacs-27.1 | |
| - coq-8.12-emacs-29.1 | |
| - coq-8.13-emacs-27.2 | |
| - coq-8.13-emacs-29.1 | |
| - coq-8.14-emacs-27.2 | |
| - coq-8.14-emacs-29.1 | |
| - coq-8.15-emacs-26.3 | |
| - coq-8.15-emacs-27.1 | |
| - coq-8.15-emacs-28.1 | |
| - coq-8.15-emacs-28.2 | |
| - coq-8.15-emacs-29.1 | |
| - coq-8.16-emacs-26.3 | |
| - coq-8.16-emacs-27.1 | |
| - coq-8.16-emacs-28.2 | |
| - coq-8.16-emacs-29.1 | |
| - coq-8.17-emacs-26.3 | |
| - coq-8.17-emacs-27.1 | |
| - coq-8.17-emacs-28.2 | |
| - coq-8.17-emacs-29.1 | |
| - coq-8.18-emacs-26.3 | |
| - coq-8.18-emacs-27.1 | |
| - coq-8.18-emacs-27.2 | |
| - coq-8.18-emacs-28.1 | |
| - coq-8.18-emacs-28.2 | |
| - coq-8.18-emacs-29.1 | |
| # 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 | |
| # don't cancel all in-progress jobs if one matrix job fails: | |
| fail-fast: false | |
| steps: | |
| - uses: actions/checkout@v2 | |
| - name: Add ert problem matcher | |
| run: echo "::add-matcher::.github/ert.json" | |
| - uses: coq-community/docker-coq-action@v1 | |
| id: docker-coq-action | |
| with: | |
| opam_file: 'dummy.opam' | |
| custom_image: proofgeneral/coq-emacs:${{matrix.coq_emacs_version}} | |
| custom_script: | | |
| startGroup Print opam config | |
| opam config list; opam repo list; opam list | |
| endGroup | |
| startGroup other relevant configuration | |
| echo getconf _NPROCESSORS_ONLN: $(getconf _NPROCESSORS_ONLN) | |
| emacs --version | |
| coqc --version | |
| ocamlc -v | |
| endGroup | |
| startGroup Run tests | |
| sudo chown -R coq:coq ./ci | |
| make tests | |
| endGroup | |
| ########################################################################### | |
| ####### compilation tests: all tests in subdirectories of ci/compile-tests | |
| ########################################################################### | |
| compile-tests: | |
| runs-on: ubuntu-latest | |
| strategy: | |
| matrix: | |
| coq_emacs_version: | |
| - coq-8.11-emacs-26.3 | |
| - coq-8.11-emacs-29.1 | |
| - coq-8.12-emacs-27.1 | |
| - coq-8.12-emacs-29.1 | |
| - coq-8.13-emacs-27.2 | |
| - coq-8.13-emacs-29.1 | |
| - coq-8.14-emacs-27.2 | |
| - coq-8.14-emacs-29.1 | |
| - coq-8.15-emacs-26.3 | |
| - coq-8.15-emacs-27.1 | |
| - coq-8.15-emacs-28.1 | |
| - coq-8.15-emacs-28.2 | |
| - coq-8.15-emacs-29.1 | |
| - coq-8.16-emacs-26.3 | |
| - coq-8.16-emacs-27.1 | |
| - coq-8.16-emacs-28.2 | |
| - coq-8.16-emacs-29.1 | |
| - coq-8.17-emacs-26.3 | |
| - coq-8.17-emacs-27.1 | |
| - coq-8.17-emacs-28.2 | |
| - coq-8.17-emacs-29.1 | |
| - coq-8.18-emacs-26.3 | |
| - coq-8.18-emacs-27.1 | |
| - coq-8.18-emacs-27.2 | |
| - coq-8.18-emacs-28.1 | |
| - coq-8.18-emacs-28.2 | |
| - coq-8.18-emacs-29.1 | |
| # don't cancel all in-progress jobs if one matrix job fails: | |
| fail-fast: false | |
| steps: | |
| - uses: actions/checkout@v2 | |
| - name: Add ert problem matcher | |
| run: echo "::add-matcher::.github/ert.json" | |
| - uses: coq-community/docker-coq-action@v1 | |
| id: docker-coq-action | |
| with: | |
| opam_file: 'dummy.opam' | |
| custom_image: proofgeneral/coq-emacs:${{matrix.coq_emacs_version}} | |
| custom_script: | | |
| startGroup other relevant configuration | |
| echo getconf _NPROCESSORS_ONLN: $(getconf _NPROCESSORS_ONLN) | |
| emacs --version | |
| coqc --version | |
| ocamlc -v | |
| endGroup | |
| startGroup Run tests | |
| sudo chown -R coq:coq ./ci | |
| make -C ci/compile-tests test | |
| endGroup | |
| ########################################################################### | |
| ####### Additional tests in ci/simple-tests for Coq | |
| ########################################################################### | |
| simple-tests: | |
| runs-on: ubuntu-latest | |
| strategy: | |
| matrix: | |
| coq_emacs_version: | |
| - coq-8.11-emacs-26.3 | |
| - coq-8.11-emacs-29.1 | |
| - coq-8.12-emacs-27.1 | |
| - coq-8.12-emacs-29.1 | |
| - coq-8.13-emacs-27.2 | |
| - coq-8.13-emacs-29.1 | |
| - coq-8.14-emacs-27.2 | |
| - coq-8.14-emacs-29.1 | |
| - coq-8.15-emacs-26.3 | |
| - coq-8.15-emacs-27.1 | |
| - coq-8.15-emacs-28.1 | |
| - coq-8.15-emacs-28.2 | |
| - coq-8.15-emacs-29.1 | |
| - coq-8.16-emacs-26.3 | |
| - coq-8.16-emacs-27.1 | |
| - coq-8.16-emacs-28.2 | |
| - coq-8.16-emacs-29.1 | |
| - coq-8.17-emacs-26.3 | |
| - coq-8.17-emacs-27.1 | |
| - coq-8.17-emacs-28.2 | |
| - coq-8.17-emacs-29.1 | |
| - coq-8.18-emacs-26.3 | |
| - coq-8.18-emacs-27.1 | |
| - coq-8.18-emacs-27.2 | |
| - coq-8.18-emacs-28.1 | |
| - coq-8.18-emacs-28.2 | |
| - coq-8.18-emacs-29.1 | |
| # don't cancel all in-progress jobs if one matrix job fails: | |
| fail-fast: false | |
| steps: | |
| - uses: actions/checkout@v2 | |
| - name: Add ert problem matcher | |
| run: echo "::add-matcher::.github/ert.json" | |
| - uses: coq-community/docker-coq-action@v1 | |
| id: docker-coq-action | |
| with: | |
| opam_file: 'dummy.opam' | |
| custom_image: proofgeneral/coq-emacs:${{matrix.coq_emacs_version}} | |
| custom_script: | | |
| startGroup other relevant configuration | |
| echo getconf _NPROCESSORS_ONLN: $(getconf _NPROCESSORS_ONLN) | |
| emacs --version | |
| coqc --version | |
| ocamlc -v | |
| endGroup | |
| startGroup Run tests | |
| sudo chown -R coq:coq ./ci | |
| make -C ci/simple-tests coq-all | |
| endGroup | |
| ########################################################################### | |
| ####### indentation tests in ci/test-indent | |
| ########################################################################### | |
| # Run indentation tests in ci/test-indent on all supported emacs | |
| # versions without coq installed. | |
| test-indent: | |
| 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/test-indent | |
| ########################################################################### | |
| ####### 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 |