-
Notifications
You must be signed in to change notification settings - Fork 9
168 lines (158 loc) · 7 KB
/
ci.yml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
# 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' }}