blob: cb195f212837977ebb136c8c19eccf1fce06a357 (
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
|
defaults:
params:
# Following parameters are used in Coq CircleCI Job (using yaml
# reference syntax)
working_directory: &workdir ~/coq
base_image: &base ocaml/opam:ubuntu-16.04_ocaml-4.05.0_flambda
# Job configuration
config: &coq
working_directory: *workdir
docker:
- image: *base
environment:
# required by some of the targets, e.g. compcert, passed for
# instance to opam to configure the number of parallel jobs
# allowed
- NJOBS: 2
version: 2
# Defines individual jobs, see the workflows section below for job orchestration
jobs:
# TODO: linter
# Build and prepare test environment
build:
<<: *coq
steps:
- checkout
# Restore last version of the dependencies in cache When a new
# major version of caches has to be generated, please use
# vYYMMDD format to avoid collision.
- restore_cache:
key: coq-opam-cache-{{ arch }}-v171208-
- run:
name: Build opam dependencies
command: |
# workaround, ought to be fixed in recent opams. See
# https://github.com/ocaml/opam/issues/2978
export TERM=xterm
opam install -y camlp5 ocamlfind
- save_cache:
key: coq-opam-cache-{{ arch }}-v171208-static-deps
paths:
- ~/.opam
- run:
name: Configure
command: |
# XXX: all this .profile stuff is a shortcoming of the
# docker image. To be improved.
. ~/.profile
./configure -local -native-compiler no
- run:
name: Build
command: |
. ~/.profile
make -j2
- run:
name: Validate
command: |
. ~/.profile
make -j2 validate
- persist_to_workspace:
root: &workspace ~/
paths:
- .opam
- coq/
bignums:
<<: *coq
steps:
# Restore workspace
- checkout
- attach_workspace:
at: *workspace
- run:
name: System dependencies
command: |
sudo apt-get update
sudo apt-get install -y python
- run:
name: Build
command: |
. ~/.profile
make -j2 ci-bignums
# bignums is a dependency
- persist_to_workspace:
root: &workspace ~/
paths:
- coq/
color:
<<: *coq
steps:
# Restore workspace
- checkout
- attach_workspace:
at: *workspace
- run:
name: System dependencies
command: |
sudo apt-get update
sudo apt-get install -y python
- run:
name: Build
command: |
. ~/.profile
make -j2 ci-color
compcert:
<<: *coq
steps:
# Restore workspace
- checkout
- attach_workspace:
at: *workspace
- run:
name: System dependencies
command: |
sudo apt-get update
sudo apt-get install -y python
- run:
name: Build
command: |
. ~/.profile
make -j2 ci-compcert
workflows:
version: 2
# Run on each push
ci:
jobs:
- build
- bignums:
requires:
- build
- color:
requires:
- build
- bignums
- compcert:
requires:
- build
|
