Skip to content

CI

CI #2180

Workflow file for this run

# This workflow will install Python dependencies, run tests and lint with a variety of Python versions
# For more information see: https://help.github.com/actions/language-and-framework-guides/using-python-with-github-actions
name: CI
on:
push:
branches: [ master ]
pull_request:
branches: [ master ]
workflow_dispatch:
schedule:
- cron: '0 8 * * *'
jobs:
build:
strategy:
fail-fast: false
matrix:
python-version: [3.6, 3.7, 3.8, 3.11, 3.12]
test-location: ['installed', 'local', 'standalone']
env:
- { COQ_VERSION: "8.15.0", COQ_PACKAGE: "coq-8.14.0", PPA: "ppa:jgross-h/many-coq-versions-ocaml-4-08", os: "ubuntu-20.04" }
- { COQ_VERSION: "8.14.1", COQ_PACKAGE: "coq-8.14.1", PPA: "ppa:jgross-h/many-coq-versions-ocaml-4-08", os: "ubuntu-20.04" }
- { COQ_VERSION: "8.13.2", COQ_PACKAGE: "coq-8.13.2", PPA: "ppa:jgross-h/many-coq-versions-ocaml-4-05", os: "ubuntu-20.04" }
- { COQ_VERSION: "8.12.2", COQ_PACKAGE: "coq-8.12.2", PPA: "ppa:jgross-h/many-coq-versions-ocaml-4-05", os: "ubuntu-20.04" }
- { COQ_VERSION: "8.11.2", COQ_PACKAGE: "coq-8.11.2", PPA: "ppa:jgross-h/many-coq-versions-ocaml-4-05", os: "ubuntu-20.04" }
- { COQ_VERSION: "8.10.2", COQ_PACKAGE: "coq-8.10.2", PPA: "ppa:jgross-h/many-coq-versions-ocaml-4-05", os: "ubuntu-20.04" }
env: ${{ matrix.env }}
runs-on: ${{ matrix.env.os }}
concurrency:
group: ${{ github.workflow }}-${{ matrix.env.COQ_VERSION }}-${{ matrix.python-version }}-${{ matrix.test-location }}-${{ github.head_ref || github.run_id }}
cancel-in-progress: true
steps:
- name: install Coq
run: |
sudo add-apt-repository "$PPA" -y
sudo apt-get -o Acquire::Retries=30 update -q
sudo apt-get -o Acquire::Retries=30 install $COQ_PACKAGE -y --allow-unauthenticated
- uses: actions/checkout@v4
- name: Set up Python ${{ matrix.python-version }}
uses: actions/setup-python@v5
with:
python-version: ${{ matrix.python-version }}
- name: Install dependencies
run: |
python -m pip install --upgrade pip
- name: Lint with flake8
run: |
python -m pip install flake8
# stop the build if there are Python syntax errors or undefined names
flake8 . --count --select=E9,F63,F7,F82 --show-source --statistics
# exit-zero treats all errors as warnings. The GitHub editor is 127 chars wide
flake8 . --count --exit-zero --max-complexity=10 --max-line-length=127 --statistics
- name: make doctests
run: make doctests PYTHON3=python
if: ${{ matrix.python-version != '2.7' }}
- name: install package building deps (pip)
run: |
python -m pip install setuptools wheel twine
if: ${{ matrix.test-location == 'installed' }}
- name: install package building deps (standalone)
run: |
python -m pip install pyinstaller
if: ${{ matrix.test-location == 'standalone' }}
- name: Build package (dist)
run: make dist
if: ${{ matrix.test-location == 'installed' }}
- name: Build package (standalone)
run: make standalone
if: ${{ matrix.test-location == 'standalone' }}
- name: Test install
run: python -m pip install .
if: ${{ matrix.test-location == 'installed' }}
- name: Test (local)
run: make print-support && make has-all-tests && make check PYTHON=python CAT_ALL_LOGS=1
if: ${{ matrix.test-location == 'local' }}
- name: Test (installed)
run: make print-support && make has-all-tests && make check PYTHON=python FIND_BUG=coq-bug-minimizer CAT_ALL_LOGS=1
if: ${{ matrix.test-location == 'installed' }}
- name: Test (standalone)
run: make print-support && make has-all-tests && make check PYTHON=python FIND_BUG=dist/coq-bug-minimizer/coq-bug-minimizer CAT_ALL_LOGS=1
if: ${{ matrix.test-location == 'standalone' }}
docker-build:
strategy:
fail-fast: false
matrix:
coq-version: ['dev', '8.20', '8.19', '8.18', '8.17', '8.16', '8.15', '8.14', '8.13', '8.12', '8.11', '8.10', '8.9', '8.8', '8.7', '8.6', '8.5', '8.4']
ocaml-version: ['default']
test-location: ['installed', 'local', 'standalone']
runs-on: ubuntu-latest
concurrency:
group: ${{ github.workflow }}-${{ matrix.coq-version }}-${{ matrix.ocaml-version }}-docker-${{ matrix.test-location }}-${{ github.head_ref || github.run_id }}
cancel-in-progress: true
steps:
- uses: actions/checkout@v4
- uses: coq-community/docker-coq-action@v1
with:
coq_version: ${{ matrix.coq-version }}
ocaml_version: ${{ matrix.ocaml-version }}
custom_script: |
sudo chmod -R a=u .
# Work around https://github.com/actions/checkout/issues/766
git config --global --add safe.directory "*"
startGroup 'install general dependencies'
sudo apt-get update -y
sudo apt-get install -y python3 python3-pip python-is-python3 python3-venv
eval $(opam env)
endGroup
startGroup 'make print-support'
make print-support
endGroup
startGroup 'coqc --help'
# Coq 8.10 and earlier error on --help, so we do `|| true`
coqc --help || true
endGroup
startGroup 'coqtop --help'
# Coq 8.10 and earlier error on --help, so we do `|| true`
coqtop --help || true
endGroup
startGroup 'setup venv'
python -m venv .venv
. .venv/bin/activate
endGroup
echo '::remove-matcher owner=coq-problem-matcher::'
if [ "${{ matrix.test-location }}" == "installed" ]; then
startGroup 'install package building deps'
python -m pip install setuptools wheel twine
endGroup
startGroup 'Build package'
make dist
endGroup
startGroup 'Test install'
python -m pip install .
endGroup
make check PYTHON=python3 FIND_BUG=coq-bug-minimizer CAT_ALL_LOGS=1
elif [ "${{ matrix.test-location }}" == "standalone" ]; then
startGroup 'install package building deps'
python -m pip install --upgrade pip
python -m pip install pyinstaller
endGroup
startGroup 'Build package'
make standalone
endGroup
make check FIND_BUG=dist/coq-bug-minimizer/coq-bug-minimizer CAT_ALL_LOGS=1
else
make check CAT_ALL_LOGS=1
fi
check-all:
runs-on: ubuntu-latest
needs: [docker-build, build]
if: always()
steps:
- run: echo 'The triggering workflow passed'
if: ${{ needs.build.result == 'success' }}
- run: echo 'The triggering workflow failed' && false
if: ${{ needs.build.result != 'success' }}
- run: echo 'The triggering workflow passed (docker)'
if: ${{ needs.docker-build.result == 'success' }}
- run: echo 'The triggering workflow failed (docker)' && false
if: ${{ needs.docker-build.result != 'success' }}