aboutsummaryrefslogtreecommitdiffhomepage
path: root/.circleci/config.yml
blob: 03aeed2eb78242f2abbc62489a4e82178e13fe59 (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
# 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: $CI_REGISTRY_IMAGE:$CACHEKEY

  environment: &envvars
    CACHEKEY: "bionic_coq-V2018-06-13-V1"
    CI_REGISTRY_IMAGE: registry.gitlab.com/coq/coq

version: 2

before_script: &before_script
  name: Setup OPAM Switch
  command: |
    echo export TERM=xterm >> ~/.profile
    source ~/.profile
    echo . ~/.profile >> $BASH_ENV
    printenv | sort
    opam switch "$COMPILER"
    opam config list
    opam list

.build-template: &build-template
  <<: *params
  steps:
    - checkout
    - run: *before_script
    - run: &build-clean
        name: Clean
        command: |
          make clean # ensure that `make clean` works on a fresh clone
    - run: &build-configure
        name: Configure
        command: |
          ./configure -local -native-compiler ${NATIVE_COMP} -coqide no
    - run: &build-build
        name: Build
        command: |
          make -j ${NJOBS} byte
          make -j ${NJOBS}
          make test-suite/misc/universes/all_stdlib.v
    - persist_to_workspace:
        root: &workspace ~/
        paths:
          - coq/

  environment:
    <<: *envvars
    NATIVE_COMP: "yes"

.ci-template: &ci-template
  <<: *params
  steps:
    - run: *before_script
    - attach_workspace: &attach_workspace
        at: *workspace

    - run:
        name: Test
        command: |
          dev/ci/ci-wrapper.sh ${CIRCLE_JOB}
    - persist_to_workspace:
        root: *workspace
        paths:
          - coq/
  environment: *envvars

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

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

  bignums:
    <<: *ci-template

  color:
    <<: *ci-template

  compcert:
    <<: *ci-template

  coq-dpdgraph:
    <<: *ci-template

  coquelicot:
    <<: *ci-template

  cross-crypto:
    <<: *ci-template

  elpi:
    <<: *ci-template

  equations:
    <<: *ci-template

  geocoq:
    <<: *ci-template

  fcsl-pcm:
    <<: *ci-template

  fiat-crypto:
    <<: *ci-template

  fiat-parsers:
    <<: *ci-template

  flocq:
    <<: *ci-template

  math-classes:
    <<: *ci-template

  corn:
    <<: *ci-template

  formal-topology:
    <<: *ci-template

  hott:
    <<: *ci-template

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

  ltac2:
    <<: *ci-template

  math-comp:
    <<: *ci-template

  mtac2:
    <<: *ci-template

  pidetop:
    <<: *ci-template

  sf:
    <<: *ci-template

  unimath:
    <<: *ci-template

  vst:
    <<: *ci-template

workflows:
  version: 2

  # Run on each push
  main:
    jobs:
      - build

      - bignums: &req-main
          requires:
            - build
      - color:
          requires:
            - build
            - bignums
      # - compcert: *req-main
      # - coq-dpdgraph: *req-main
      # - coquelicot: *req-main
      # - cross-crypto: *req-main
      # - elpi: *req-main
      # - equations: *req-main
      # - geocoq: *req-main
      # - fcsl-pcm: *req-main
      # - fiat-crypto: *req-main
      # - fiat-parsers: *req-main
      # - flocq: *req-main
      - math-classes:
          requires:
            - build
            - bignums
      # - mtac2: *req-main
      - 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
      # - pidetop: *req-main
      # - sf: *req-main
      # - unimath: *req-main
      # - vst: *req-main