-
Notifications
You must be signed in to change notification settings - Fork 5
208 lines (180 loc) · 6.8 KB
/
main.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
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
# This is a basic workflow to help you get started with Actions
name: CI
# Controls when the workflow will run
on:
# Triggers the workflow on push or pull request events but only for the "main" branch
push:
branches:
- main
paths-ignore:
- 'README.org'
- 'Notes/*'
pull_request:
branches:
- main
paths-ignore:
- 'README.org'
- 'Notes/*'
# Allows you to run this workflow manually from the Actions tab
workflow_dispatch:
########################################################################
## CONFIGURATION
##
## See SETTINGS for the most important configuration variable: AGDA_BRANCH.
## It has to be defined as a build step because it is potentially branch
## dependent.
##
## As for the rest:
##
## Basically do not touch GHC_VERSION and CABAL_VERSION as long as
## they aren't a problem in the build. If you have time to waste, it
## could be worth investigating whether newer versions of ghc produce
## more efficient Agda executable and could cut down the build time.
## Just be aware that actions are flaky and small variations are to be
## expected.
##
## The CABAL_INSTALL variable only passes `-O1` optimisations to ghc
## because github actions cannot currently handle a build using `-O2`.
## To be experimented with again in the future to see if things have
## gotten better.
##
########################################################################
########################################################################
## SETTINGS
##
## AGDA_BRANCH picks the branch of Agda to use to build the library.
## It doesn't really track the branch, so you have to drop caches to
## get a new branch version if it changes. This will be fixed in the
## next PR.
########################################################################
env:
AGDA_BRANCH: v2.6.3
GHC_VERSION: 9.2.5
CABAL_VERSION: 3.6.2.0
CABAL_INSTALL: cabal install --overwrite-policy=always --ghc-options='-O1 +RTS -M6G -RTS'
CACHE_PATHS: |
~/.cabal/packages
~/.cabal/store
~/.cabal/bin
# A workflow run is made up of one or more jobs that can run sequentially or in parallel
jobs:
line-lengths:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v3
- name: Set up Python 3.8
uses: actions/setup-python@v2
with:
python-version: 3.8
- name: Install dependencies
run: |
python -m pip install --upgrade pip
pip install wcwidth
- name: Check line lengths
run: |
error=0
shopt -s globstar nullglob
for file in **/*.agda; do
python3 -c '
import sys
from wcwidth import wcswidth
filename = sys.argv[1]
try:
with open(filename, "r", encoding="utf-8") as file:
for lineno, line in enumerate(file, 1):
if wcswidth(line.rstrip("\n")) > 80:
print(f"{filename}:{lineno}: line too long")
sys.exit(1)
except Exception as e:
print(f"Error processing {filename}: {e}")
sys.exit(1)
' "${file}" || error=1
done
exit ${error}
compile-agda:
runs-on: ubuntu-latest
steps:
- name: Install cabal
uses: haskell/actions/setup@v2
with:
ghc-version: ${{ env.GHC_VERSION }}
cabal-version: ${{ env.CABAL_VERSION }}
cabal-update: true
# This caching step allows us to save a lot of building time by only
# rebuilding Agda, and re-checking unchanged library files if
# absolutely necessary i.e. if we change either the version of Agda,
# ghc, or cabal that we want to use for the build.
- name: Restore external dependencies cache
uses: actions/cache/restore@v3
id: cache-external-restore
with:
path: ${{ env.CACHE_PATHS }}
key: ${{ runner.os }}-${{ env.GHC_VERSION }}-${{ env.CABAL_VERSION }}-${{ env.AGDA_BRANCH }}
########################################################################
## INSTALLATION STEPS
########################################################################
- name: Download and install Agda from github
if: steps.cache-external-restore.outputs.cache-hit != 'true'
run: |
git clone https://github.com/agda/agda --branch ${{ env.AGDA_BRANCH }} --depth=1
cd agda
mkdir -p doc
touch doc/user-manual.pdf
${{ env.CABAL_INSTALL }}
cd ..
rm -rf agda
- name: Download Agda Standard Library from github
run : |
cd ~
git clone https://github.com/agda/agda-stdlib.git
echo "AGDA_STDLIB_DIR=$PWD/agda-stdlib" >> "$GITHUB_ENV"
- name: Download Cubical from github
run : |
cd ~
git clone https://github.com/agda/cubical --branch master
echo "CUBICAL_DIR=$PWD/cubical" >> "$GITHUB_ENV"
- name: Set up Agda dependencies
run : |
mkdir ~/.agda
touch ~/.agda/libraries
echo "$CUBICAL_DIR/cubical.agda-lib" >> ~/.agda/libraries
echo "$AGDA_STDLIB_DIR/standard-library.agda-lib" >> ~/.agda/libraries
echo "$GITHUB_WORKSPACE/multi-poly-cats.agda-lib" >> ~/.agda/libraries
- name: Download and install fix-whitespace
if: steps.cache-external-restore.outputs.cache-hit != 'true'
run: |
cd ~
git clone https://github.com/agda/fix-whitespace --depth=1
cd fix-whitespace
${{ env.CABAL_INSTALL }} fix-whitespace.cabal
cd ..
- name: Cache External Dependencies
if: steps.cache-external-restore.outputs.cache-hit != 'true'
uses: actions/cache/save@v3
id: cache-external-save
with:
path: ${{ env.CACHE_PATHS }}
key: ${{ steps.cache-external-restore.outputs.cache-primary-key }}
########################################################################
## CHECKOUT
########################################################################
# By default github actions do not pull the repo
- name: Checkout multi-poly-cats
uses: actions/checkout@v3
########################################################################
## TESTING
########################################################################
- name: Put cabal programs in PATH
run: echo "~/.cabal/bin" >> $GITHUB_PATH
- name: Cache Agdai Files
uses: actions/cache@v3
with:
path: '**/*.agdai'
key: ${{ runner.os }}-agdai-${{ hashFiles('**/*.agda') }}
restore-keys: |
${{ runner.os }}-agdai-
- name: Test multi-poly-cats
run: |
make test \
AGDA='~/.cabal/bin/agda -WnoUnsupportedIndexedMatch -W error' \
FIX_WHITESPACE='~/.cabal/bin/fix-whitespace'