proof-stat: address review comments #219
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
| # 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: | |
| push: | |
| branches: | |
| #- master | |
| #- hybrid | |
| - "**" | |
| pull_request: | |
| branches: | |
| - '**' | |
| jobs: | |
| ########################################################################### | |
| ####### compile and build manual | |
| ########################################################################### | |
| build: | |
| runs-on: ubuntu-latest | |
| 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 | |
| - 29.2 | |
| # CIPG change marker end | |
| # 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. | |
| # | |
| # 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.2 | |
| # CIPG change marker end | |
| # 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: | |
| # 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.2-emacs-26.3 | |
| - coq-8.11.2-emacs-29.2 | |
| - coq-8.12.2-emacs-27.1 | |
| - coq-8.12.2-emacs-29.2 | |
| - coq-8.13.2-emacs-27.2 | |
| - coq-8.13.2-emacs-29.2 | |
| - coq-8.14.1-emacs-27.2 | |
| - coq-8.14.1-emacs-29.2 | |
| - coq-8.15.2-emacs-27.1 | |
| - coq-8.15.2-emacs-28.1 | |
| - coq-8.15.2-emacs-29.2 | |
| - coq-8.16.1-emacs-26.3 | |
| - coq-8.16.1-emacs-27.1 | |
| - coq-8.16.1-emacs-28.2 | |
| - coq-8.16.1-emacs-29.2 | |
| - coq-8.17.1-emacs-26.3 | |
| - coq-8.17.1-emacs-27.1 | |
| - coq-8.17.1-emacs-28.2 | |
| - coq-8.17.1-emacs-29.1 | |
| - coq-8.17.1-emacs-29.2 | |
| - coq-8.18.0-emacs-26.3 | |
| - coq-8.18.0-emacs-27.1 | |
| - coq-8.18.0-emacs-28.2 | |
| - coq-8.18.0-emacs-29.1 | |
| - coq-8.18.0-emacs-29.2 | |
| - coq-8.19.1-emacs-26.3 | |
| - coq-8.19.1-emacs-27.1 | |
| - coq-8.19.1-emacs-27.2 | |
| - coq-8.19.1-emacs-28.1 | |
| - coq-8.19.1-emacs-28.2 | |
| - coq-8.19.1-emacs-29.1 | |
| - coq-8.19.1-emacs-29.2 | |
| # CIPG change marker end | |
| # 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: | |
| # 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.2-emacs-26.3 | |
| - coq-8.11.2-emacs-29.2 | |
| - coq-8.12.2-emacs-27.1 | |
| - coq-8.12.2-emacs-29.2 | |
| - coq-8.13.2-emacs-27.2 | |
| - coq-8.13.2-emacs-29.2 | |
| - coq-8.14.1-emacs-27.2 | |
| - coq-8.14.1-emacs-29.2 | |
| - coq-8.15.2-emacs-27.1 | |
| - coq-8.15.2-emacs-28.1 | |
| - coq-8.15.2-emacs-29.2 | |
| - coq-8.16.1-emacs-26.3 | |
| - coq-8.16.1-emacs-27.1 | |
| - coq-8.16.1-emacs-28.2 | |
| - coq-8.16.1-emacs-29.2 | |
| - coq-8.17.1-emacs-26.3 | |
| - coq-8.17.1-emacs-27.1 | |
| - coq-8.17.1-emacs-28.2 | |
| - coq-8.17.1-emacs-29.1 | |
| - coq-8.17.1-emacs-29.2 | |
| - coq-8.18.0-emacs-26.3 | |
| - coq-8.18.0-emacs-27.1 | |
| - coq-8.18.0-emacs-28.2 | |
| - coq-8.18.0-emacs-29.1 | |
| - coq-8.18.0-emacs-29.2 | |
| - coq-8.19.1-emacs-26.3 | |
| - coq-8.19.1-emacs-27.1 | |
| - coq-8.19.1-emacs-27.2 | |
| - coq-8.19.1-emacs-28.1 | |
| - coq-8.19.1-emacs-28.2 | |
| - coq-8.19.1-emacs-29.1 | |
| - coq-8.19.1-emacs-29.2 | |
| # CIPG change marker end | |
| # 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: | |
| # 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.2-emacs-26.3 | |
| - coq-8.11.2-emacs-29.2 | |
| - coq-8.12.2-emacs-27.1 | |
| - coq-8.12.2-emacs-29.2 | |
| - coq-8.13.2-emacs-27.2 | |
| - coq-8.13.2-emacs-29.2 | |
| - coq-8.14.1-emacs-27.2 | |
| - coq-8.14.1-emacs-29.2 | |
| - coq-8.15.2-emacs-27.1 | |
| - coq-8.15.2-emacs-28.1 | |
| - coq-8.15.2-emacs-29.2 | |
| - coq-8.16.1-emacs-26.3 | |
| - coq-8.16.1-emacs-27.1 | |
| - coq-8.16.1-emacs-28.2 | |
| - coq-8.16.1-emacs-29.2 | |
| - coq-8.17.1-emacs-26.3 | |
| - coq-8.17.1-emacs-27.1 | |
| - coq-8.17.1-emacs-28.2 | |
| - coq-8.17.1-emacs-29.1 | |
| - coq-8.17.1-emacs-29.2 | |
| - coq-8.18.0-emacs-26.3 | |
| - coq-8.18.0-emacs-27.1 | |
| - coq-8.18.0-emacs-28.2 | |
| - coq-8.18.0-emacs-29.1 | |
| - coq-8.18.0-emacs-29.2 | |
| - coq-8.19.1-emacs-26.3 | |
| - coq-8.19.1-emacs-27.1 | |
| - coq-8.19.1-emacs-27.2 | |
| - coq-8.19.1-emacs-28.1 | |
| - coq-8.19.1-emacs-28.2 | |
| - coq-8.19.1-emacs-29.1 | |
| - coq-8.19.1-emacs-29.2 | |
| # CIPG change marker end | |
| # 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: | |
| # 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 | |
| - 29.2 | |
| # CIPG change marker end | |
| # 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: | |
| # 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 | |
| - 29.2 | |
| # CIPG change marker end | |
| # 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 |