Skip to content
CI

proof-stat: admitted proofs should count as failing #241

Sign in to view logs

proof-stat: admitted proofs should count as failing

proof-stat: admitted proofs should count as failing #241

Workflow file for this run

.github/workflows/test.yml at 9e9f499
# 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
- 29.3
# 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.3
# 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.3
- coq-8.12.2-emacs-27.1
- coq-8.12.2-emacs-29.3
- coq-8.13.2-emacs-27.2
- coq-8.13.2-emacs-29.3
- coq-8.14.1-emacs-27.2
- coq-8.14.1-emacs-29.3
- coq-8.15.2-emacs-27.1
- coq-8.15.2-emacs-28.1
- coq-8.15.2-emacs-29.3
- 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.3
- 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.3
- 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.3
- 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
- coq-8.19.1-emacs-29.3
# 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 .
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.3
- coq-8.12.2-emacs-27.1
- coq-8.12.2-emacs-29.3
- coq-8.13.2-emacs-27.2
- coq-8.13.2-emacs-29.3
- coq-8.14.1-emacs-27.2
- coq-8.14.1-emacs-29.3
- coq-8.15.2-emacs-27.1
- coq-8.15.2-emacs-28.1
- coq-8.15.2-emacs-29.3
- 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.3
- 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.3
- 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.3
- 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
- coq-8.19.1-emacs-29.3
# 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 .
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.3
- coq-8.12.2-emacs-27.1
- coq-8.12.2-emacs-29.3
- coq-8.13.2-emacs-27.2
- coq-8.13.2-emacs-29.3
- coq-8.14.1-emacs-27.2
- coq-8.14.1-emacs-29.3
- coq-8.15.2-emacs-27.1
- coq-8.15.2-emacs-28.1
- coq-8.15.2-emacs-29.3
- 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.3
- 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.3
- 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.3
- 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
- coq-8.19.1-emacs-29.3
# 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 .
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
- 29.3
# 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
- 29.3
# 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