aboutsummaryrefslogtreecommitdiffhomepage
path: root/.circleci/config.yml
blob: 352ec5a51a980007a3c243fdf6c3a27ccfeed50f (plain)
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
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
# This file used to contain configuration to also build documentation and CoqIDE,
# run the test-suite and the validate targets,
# including with 32-bits architecture or bleeding-edge compiler.

defaults:
  params: &params
    # Following parameters are used in Coq CircleCI Job (using yaml
    # reference syntax)
    working_directory: ~/coq
    docker:
      - image: ocaml/opam:ubuntu

  environment: &envvars
    # required by some of the targets, e.g. compcert, passed for
    # instance to opam to configure the number of parallel jobs
    # allowed
    NJOBS: 2
    COMPILER: "system"
    CAMLP5_VER: "6.14"
    NATIVE_COMP: "yes"

    # some useful values
    TIMING_PACKAGES: &timing-packages "time python"

version: 2

before_script: &before_script
  name: Install system packages
  command: |
    echo export TERM=xterm >> ~/.profile
    source ~/.profile
    printenv
    if [ -n "${EXTRA_PACKAGES}" ]; then sudo apt-get update -yq && sudo apt-get install -yq --no-install-recommends ${EXTRA_PACKAGES}; fi

opam-switch: &opam-switch
  name: Select opam switch
  command: |
    source ~/.profile
    opam switch ${COMPILER}
    opam config list
    opam list

.opam-boot-template: &opam-boot-template
  <<: *params
  steps:
    - checkout
    - run: *before_script
    - run:
        name: Cache selection
        command: |
          source ~/.profile
          # We can't use environment variables in cache names
          # So put it in a file and use the checksum
          echo "$COMPILER" > COMPILER
    - restore_cache:
        keys:
          - coq-opam-cache-v1-{{ arch }}-{{ checksum "COMPILER" }}-{{ checksum ".circleci/config.yml" }}-
          - coq-opam-cache-v1-{{ arch }}-{{ checksum "COMPILER" }}- # this grabs old cache if checksum doesn't match
    - run:
        name: Update opam lists
        command: |
          source ~/.profile
          opam repository set-url default https://opam.ocaml.org
          opam update
    - run:
        name: Install opam packages
        command: |
          source ~/.profile
          opam switch -j ${NJOBS} ${COMPILER}
          opam install -j ${NJOBS} -y camlp5.${CAMLP5_VER} ocamlfind ${EXTRA_OPAM}
    - run:
        name: Clean cache
        command: |
          source ~/.profile
          rm -rf ~/.opam/log/
    - save_cache:
        key: coq-opam-cache-v1-{{ arch }}-{{ checksum "COMPILER" }}-{{ checksum ".circleci/config.yml" }}-
        paths:
          - ~/.opam
    - persist_to_workspace:
        root: &workspace ~/
        paths:
          - .opam/

.build-template: &build-template
  <<: *params
  steps:
    - checkout
    - run: *before_script
    - attach_workspace: &attach_workspace
        at: *workspace
    - run: *opam-switch
    - run: &build-configure
        name: Configure
        command: |
          source ~/.profile

          ./configure -local -native-compiler ${NATIVE_COMP} -coqide no
    - run: &build-build
        name: Build
        command: |
          source ~/.profile
          make -j ${NJOBS} byte
          make -j ${NJOBS}
          make test-suite/misc/universes/all_stdlib.v
    - persist_to_workspace:
        root: *workspace
        paths:
          - coq/

  environment: *envvars

.ci-template: &ci-template
  <<: *params
  steps:
    - run: *before_script
    - attach_workspace: *attach_workspace
    - run:
        name: Test
        command: |
          source ~/.profile
          dev/ci/ci-wrapper.sh ${CIRCLE_JOB}
    - persist_to_workspace:
        root: *workspace
        paths:
          - coq/
  environment: &ci-template-vars
    <<: *envvars
    EXTRA_PACKAGES: *timing-packages

# Defines individual jobs, see the workflows section below for job orchestration
jobs:

  opam-boot:
    <<: *opam-boot-template
    environment:
      <<: *envvars
      EXTRA_OPAM: "ocamlgraph ppx_tools_versioned ppx_deriving ocaml-migrate-parsetree"

  # Build and prepare test environment
  build: *build-template

  bignums:
    <<: *ci-template

  color:
    <<: *ci-template
    environment:
      <<: *ci-template-vars
      EXTRA_PACKAGES: *timing-packages

  compcert:
    <<: *ci-template

  coq-dpdgraph:
    <<: *ci-template
    environment:
      <<: *ci-template-vars
      EXTRA_PACKAGES: "time python autoconf automake"

  coquelicot:
    <<: *ci-template
    environment:
      <<: *ci-template-vars
      EXTRA_PACKAGES: "time python autoconf automake"

  elpi:
    <<: *ci-template

  equations:
    <<: *ci-template

  geocoq:
    <<: *ci-template

  fiat-crypto:
    <<: *ci-template

  fiat-parsers:
    <<: *ci-template
    environment:
      <<: *ci-template-vars
      EXTRA_PACKAGES: *timing-packages

  flocq:
    <<: *ci-template
    environment:
      <<: *ci-template-vars
      EXTRA_PACKAGES: "time python autoconf automake"

  math-classes:
    <<: *ci-template

  corn:
    <<: *ci-template

  formal-topology:
    <<: *ci-template

  hott:
    <<: *ci-template
    environment:
      <<: *ci-template-vars
      EXTRA_PACKAGES: "time python autoconf automake"

  iris-lambda-rust:
    <<: *ci-template

  ltac2:
    <<: *ci-template

  math-comp:
    <<: *ci-template

  sf:
    <<: *ci-template
    environment:
      <<: *ci-template-vars
      EXTRA_PACKAGES: "time python wget"

  unimath:
    <<: *ci-template

  vst:
    <<: *ci-template

workflows:
  version: 2
  # Run on each push
  main:
    jobs:
      - opam-boot

      - build:
          requires:
            - opam-boot

      - bignums: &req-main
          requires:
            - build
      - color:
          requires:
            - build
            - bignums
      - compcert: *req-main
      - coq-dpdgraph: *req-main
      - coquelicot: *req-main
      - elpi: *req-main
      - equations: *req-main
      - geocoq: *req-main
      - fiat-crypto: *req-main
      - fiat-parsers: *req-main
      - flocq: *req-main
      - math-classes:
          requires:
            - build
            - bignums
      - corn:
          requires:
            - build
            - math-classes
      - formal-topology:
          requires:
            - build
            - corn
      - hott: *req-main
      - iris-lambda-rust: *req-main
      - ltac2: *req-main
      - math-comp: *req-main
      - sf: *req-main
      - unimath: *req-main
      - vst: *req-main