This repository has been archived by the owner on Aug 6, 2024. It is now read-only.
forked from UniMath/UniMath
-
Notifications
You must be signed in to change notification settings - Fork 0
208 lines (181 loc) · 6.95 KB
/
build-unimath.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
name: CI Build UniMath
on:
push:
branches: [master]
pull_request:
branches: [master]
# Allows you to run this workflow manually from the Actions tab
workflow_dispatch:
schedule:
# Based on https://github.com/marketplace/actions/set-up-ocaml
# Prime the caches every Monday
- cron: '0 1 * * MON'
concurrency:
group: ${{ github.workflow }}-${{ github.ref }}
cancel-in-progress: true
jobs:
# This workflow contains four kinds of jobs:
# - sanity-checks
# - build-Unimath-ubuntu: (Linux, docker-coq, latest Coq >= 8.16, manual cache)
# - build-macos: (MacOS, Opam, Coq 8.16.0, cache using actions/setup-ocaml)
# - build-satellites: (Linux, docker-coq, Coq 8.16.x, manual cache)
sanity-checks:
name: Sanity Checks
runs-on: ubuntu-22.04
steps:
- uses: actions/checkout@v4
- name: Install build dependencies
run: |
sudo apt-get update
sudo apt-get install coq
type coqc
coqc --version
- name: Run sanity checks
run: |
cd $GITHUB_WORKSPACE
time make -k sanity-checks || time make sanity-checks
# Build the current PR/branch with the latest stable release of Coq.
build-Unimath-ubuntu:
strategy:
fail-fast: false
matrix:
os: [ubuntu-22.04]
# https://github.com/coq-community/docker-coq/wiki#ocaml-versions-policy
coq-version: [latest, 8.20-alpha, dev]
# (the following is obsolete:) coq-version: [8.16] or [latest, 8.16] (when 8.17 is released)
ocaml-version: [default]
name: Build on Linux (Coq ${{ matrix.coq-version }})
runs-on: ${{ matrix.os }}
steps:
- uses: actions/checkout@v4
# Grab the cache if available and extract it to dune-cache/. We tell dune
# to use $(pwd)/dune-cache/ in the custom_script when initiating the
# docker run.
- uses: actions/cache/restore@v4
id: cache
with:
path: dune-cache
# Example key: UniMath-Linux-coq-8.16-123456789-10
key: UniMath-${{ runner.os }}-coq-${{ matrix.coq-version }}-${{ github.run_id }}-${{ github.run_number }}
restore-keys: |
UniMath-${{ runner.os }}-coq-${{ matrix.coq-version }}-${{ github.run_id }}
UniMath-${{ runner.os }}-coq-${{ matrix.coq-version }}-
- name: Build UniMath
uses: coq-community/docker-coq-action@v1
with:
coq_version: ${{ matrix.coq-version }}
ocaml_version: ${{ matrix.ocaml-version }}
custom_script: |
startGroup "Workaround permission issue"
sudo chown -R coq:coq .
endGroup
startGroup "Print versions"
opam --version
opam exec -- dune --version
opam exec -- coqc --version
endGroup
startGroup "Build UniMath"
export DUNE_CACHE_ROOT=$(pwd)/dune-cache/
opam exec -- dune build -j 2 --display=short \
--cache=enabled --error-reporting=twice
endGroup
- name: Revert permissions
if: ${{ always() }}
run: sudo chown -R 1001:116 .
- uses: actions/cache/save@v4
if: always()
with:
path: dune-cache
key: UniMath-${{ runner.os }}-coq-${{ matrix.coq-version }}-${{ github.run_id }}-${{ github.run_number }}
# Build UniMath on MacOS using latest stable release of Coq installed with
# Homebrew (8.18.0 still on March 18, 2024). Build files are cached.
build-macos:
name: Build on macOS (latest Coq on Homebrew)
runs-on: macos-latest
steps:
- uses: actions/checkout@v4
- name: Install Coq
run: |
brew install coq ocaml-findlib dune
coqc --version
dune --version
- uses: actions/cache/restore@v4
id: cache
with:
path: dune-cache
key: UniMath-MacOS-${{ github.run_id }}-${{ github.run_number }}
restore-keys: |
UniMath-MacOS-${{ github.run_id }}
UniMath-MacOS
- name: Build UniMath
run: |
export DUNE_CACHE_ROOT=$(pwd)/dune-cache/
dune build --display=short --error-reporting=twice --cache=enabled UniMath/
- uses: actions/cache/save@v4
if: always ()
with:
path: dune-cache
key: UniMath-MacOS-${{ github.run_id }}-${{ github.run_number }}
# Build the satellites in parallel using docker-coq images with the latest
# stable patch-release of Coq 8.19 as of March 20, 2024
# (outdated comment:) except for TypeTheory, which is built
# using the latest stable 8.15 release.
build-satellites:
strategy:
fail-fast: false
matrix:
satellite: [SetHITs, largecatmodules, GrpdHITs, TypeTheory]
coq-version: [latest, 8.20-alpha, dev]
ocaml-version: [default]
# (outdated exception:) exclude:
# - satellite: GrpdHITs
# coq-version: dev
name: Build ${{ matrix.satellite }} (Coq ${{ matrix.coq-version }})
runs-on: ubuntu-22.04
steps:
# Check out the current branch of UniMath in the current directory.
- uses: actions/checkout@v4
# Check out the satellite we want to build in Satellite/.
- name: Clone ${{ matrix.satellite }}
uses: actions/checkout@v4
with:
repository: UniMath/${{ matrix.satellite }}
path: Satellite
# Grab the cache if available. We tell dune to use $(pwd)/dune-cache/ in
# the custom_script below.
- uses: actions/cache/restore@v4
id: cache
with:
path: dune-cache
# Example key: SetHITs-coq-8.15-123456789-10
key: ${{ matrix.satellite }}-coq-${{ matrix.coq-version }}-${{ github.run_id }}-${{ github.run_number }}
restore-keys: |
${{ matrix.satellite }}-coq-${{ matrix.coq-version }}-${{ github.run_id }}
${{ matrix.satellite }}-coq-${{ matrix.coq-version }}-
- name: Build ${{ matrix.satellite }}
uses: coq-community/docker-coq-action@v1
with:
coq_version: ${{ matrix.coq-version }}
ocaml_version: ${{ matrix.ocaml-version }}
custom_script: |
startGroup "Workaround permission issue"
sudo chown -R coq:coq .
endGroup
startGroup "Print versions"
opam --version
opam exec -- dune --version
opam exec -- coqc --version
endGroup
startGroup "Build Satellite"
export DUNE_CACHE_ROOT=$(pwd)/dune-cache/
opam exec -- dune build -j 2 Satellite --display=short \
--cache=enabled --error-reporting=twice
endGroup
- name: Revert permissions
if: ${{ always() }}
run: sudo chown -R 1001:116 .
- uses: actions/cache/save@v4
if: always ()
with:
path: dune-cache
key: ${{ matrix.satellite }}-coq-${{ matrix.coq-version }}-${{ github.run_id }}-${{ github.run_number }}