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
|
name: Ubuntu build
on:
push:
branches:
- master
- experimental
- 'v*-release'
pull_request:
branches:
- master
- experimental
merge_group:
########################################################################
## CONFIGURATION
##
## See SETTINGS for the most important configuration variable: AGDA_COMMIT.
## 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.
##
## We mostly use `v1-install` rather than `install` as Agda as a community
## hasn't figured out how to manage dependencies with the new local
## style builds (see agda/agda#4627 for details). Once this is resolved
## we should upgrade to `install`.
##
## The AGDA variable specifies the command to use to build the library.
## It currently passes the flag `-Werror` to ensure maximal compliance
## with e.g. not relying on deprecated definitions.
## The rest are some arbitrary runtime arguments that shape the way Agda
## allocates and garbage collects memory. It should make things faster.
## Limits can be bumped if the builds start erroring with out of memory
## errors.
##
########################################################################
env:
GHC_VERSION: 9.10.1
CABAL_VERSION: 3.12.1.0
CABAL_V1_INSTALL: cabal v1-install --ghc-options='-O1 +RTS -M6G -RTS'
CABAL_INSTALL: cabal install --overwrite-policy=always --ghc-options='-O1 +RTS -M6G -RTS'
AGDA: agda -Werror +RTS -M5G -H3.5G -A128M -RTS -i. -isrc -idoc
jobs:
test-stdlib:
runs-on: ubuntu-latest
steps:
########################################################################
## SETTINGS
##
## AGDA_COMMIT picks the version of Agda to use to build the library.
## It can either be a hash of a specific commit (to target a bugfix for
## instance) or a tag e.g. tags/v2.6.1.3 (to target a released version).
##
## AGDA_HTML_DIR picks the html/ subdir in which to publish the docs.
## The content of the html/ directory will be deployed so we put the
## master version at the root and the experimental in a subdirectory.
########################################################################
- name: Initialise variables
run: |
if [[ '${{ github.ref }}' == 'refs/heads/experimental' \
|| '${{ github.base_ref }}' == 'experimental' ]]; then
# Pick Agda version for experimental
echo "AGDA_COMMIT=ef912c68fd329ad3046d156e3c1a70a7fec19ba1" >> "${GITHUB_ENV}";
echo "AGDA_HTML_DIR=html/experimental" >> "${GITHUB_ENV}"
else
# Pick Agda version for master
echo "AGDA_COMMIT=tags/v2.8.0-rc3" >> "${GITHUB_ENV}";
echo "AGDA_HTML_DIR=html/master" >> "${GITHUB_ENV}"
fi
if [[ '${{ github.ref }}' == 'refs/heads/master' \
|| '${{ github.ref }}' == 'refs/heads/experimental' ]]; then
echo "AGDA_DEPLOY=true" >> "${GITHUB_ENV}"
fi
########################################################################
## CACHING
########################################################################
# This caching step allows us to save a lot of building time by only
# downloading ghc and cabal and rebuilding Agda 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: Cache ~/.cabal directories
uses: actions/cache@v4
id: cache-cabal
with:
path: |
~/.cabal/packages
~/.cabal/store
~/.cabal/bin
~/.cabal/share
key: ${{ runner.os }}-${{ env.GHC_VERSION }}-${{ env.CABAL_VERSION }}-${{ env.AGDA_COMMIT }}-cache
########################################################################
## INSTALLATION STEPS
########################################################################
- name: Install ghc & cabal
uses: haskell-actions/setup@v2
with:
ghc-version: ${{ env.GHC_VERSION }}
cabal-version: ${{ env.CABAL_VERSION }}
cabal-update: true
- name: Put cabal programs in PATH
run: echo ~/.cabal/bin >> "${GITHUB_PATH}"
- name: Install alex & happy
if: steps.cache-cabal.outputs.cache-hit != 'true'
run: |
${{ env.CABAL_INSTALL }} alex
${{ env.CABAL_INSTALL }} happy
# happy>=2.0 cannot be v1-installed: https://github.com/haskell/happy/issues/315
# Since we only need the executable, it is fine to use v2-install here.
- name: Download and install Agda from github
if: steps.cache-cabal.outputs.cache-hit != 'true'
run: |
git clone https://github.com/agda/agda
cd agda
git checkout ${{ env.AGDA_COMMIT }}
mkdir -p doc
touch doc/user-manual.pdf
${{ env.CABAL_V1_INSTALL }}
cd ..
########################################################################
## TESTING
########################################################################
# By default github actions do not pull the repo
- name: Checkout stdlib
uses: actions/checkout@v4
- name: Test stdlib
run: |
# Including deprecated modules purely for testing
cabal run GenerateEverything -- --include-deprecated
${{ env.AGDA }} -WnoUserWarning --safe EverythingSafe.agda
${{ env.AGDA }} -WnoUserWarning Everything.agda
- name: Prepare HTML index
run: |
# Regenerating the Everything files without the deprecated modules
cabal run GenerateEverything
cp .github/tooling/* .
./index.sh
${{ env.AGDA }} --safe EverythingSafe.agda
${{ env.AGDA }} Everything.agda
${{ env.AGDA }} index.agda
- name: Golden testing
run: |
${{ env.CABAL_V1_INSTALL }} clock
make testsuite INTERACTIVE='' AGDA_EXEC='~/.cabal/bin/agda'
########################################################################
## DOC DEPLOYMENT
########################################################################
# We start by retrieving the currently deployed docs
# We remove the content that is in the directory we are going to populate
# so that stale files corresponding to deleted modules do not accumulate.
# We then generate the docs in the AGDA_HTML_DIR subdirectory
- name: Generate HTML
run: |
git clone --depth 1 --single-branch --branch gh-pages https://github.com/agda/agda-stdlib html
rm -f '${{ env.AGDA_HTML_DIR }}'/*.html
rm -f '${{ env.AGDA_HTML_DIR }}'/*.css
${{ env.AGDA }} --html --html-dir ${{ env.AGDA_HTML_DIR }} index.agda
cp .github/tooling/* .
./landing.sh
- name: Deploy HTML
uses: JamesIves/github-pages-deploy-action@v4
if: success() && env.AGDA_DEPLOY
with:
branch: gh-pages
folder: html
git-config-name: Github Actions
|
