-
Notifications
You must be signed in to change notification settings - Fork 2
/
.gitlab-ci.yml
157 lines (132 loc) · 4.29 KB
/
.gitlab-ci.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
image: "coqorg/coq:latest"
variables:
DIGGER_BRANCH: master
DX_BRANCH: main
build x86 minimal with digger:
stage: build
script:
- opam config list
- opam list
# get digger from latest CI artifacts
- cd tools/digger
- curl -L "https://gitlab.univ-lille.fr/2xs/digger/-/jobs/artifacts/$DIGGER_BRANCH/download?job=build" -o digger.zip
- unzip -oq digger.zip
- ./digger --version
- cd ../..
- .ci/apt-get.sh nasm gcc
- coqc --version
- ./configure.sh --architecture=x86 --partition-name=minimal --libpip=/tmp --c-compiler=gcc --linker=ld --no-command-check
- make minimal.elf
artifacts:
paths:
- minimal.elf
expire_in: 1 hour
build arm minimal with digger:
stage: build
script:
- opam config list
- opam list
# get digger from latest CI artifacts
- cd tools/digger
- curl -L "https://gitlab.univ-lille.fr/2xs/digger/-/jobs/artifacts/$DIGGER_BRANCH/download?job=build" -o digger.zip
- unzip -oq digger.zip
- ./digger --version
- cd ../..
- .ci/apt-get.sh libnewlib-arm-none-eabi gcc-arm-none-eabi
- coqc --version
- ./configure.sh --architecture=armv7 --partition-name=minimal --libpip=/tmp --no-command-check
- make minimal.elf
artifacts:
paths:
- minimal.elf
expire_in: 1 hour
build x86 minimal with dx:
stage: build
script:
- opam config list
- opam list
- LIB=$(opam var lib)
# get dx from latest CI artifacts
- cd .ci
- echo "Download dx artifact from https://gitlab.univ-lille.fr/2xs/dx/-/jobs/artifacts/$DX_BRANCH/download?job=build%20dx%20and%20deps"
- curl -L "https://gitlab.univ-lille.fr/2xs/dx/-/jobs/artifacts/$DX_BRANCH/download?job=build%20dx%20and%20deps" -o dx.zip
- unzip -oq dx.zip
- rsync -rpt dx-and-deps/* $LIB
- cd ..
- .ci/apt-get.sh nasm gcc
- coqc --version
- ./configure.sh --architecture=x86 --partition-name=minimal --libpip=/tmp --dx=$LIB/dx --c-compiler=gcc --linker=ld --no-command-check
- make minimal.elf
artifacts:
paths:
- minimal.elf
expire_in: 1 hour
build arm minimal with dx:
stage: build
script:
- opam config list
- opam list
- LIB=$(opam var lib)
# get dx from latest CI artifacts
- cd .ci
- echo "Download dx artifact from https://gitlab.univ-lille.fr/2xs/dx/-/jobs/artifacts/$DX_BRANCH/download?job=build%20dx%20and%20deps"
- curl -L "https://gitlab.univ-lille.fr/2xs/dx/-/jobs/artifacts/$DX_BRANCH/download?job=build%20dx%20and%20deps" -o dx.zip
- unzip -oq dx.zip
- rsync -rpt dx-and-deps/* $LIB
- cd ..
- .ci/apt-get.sh libnewlib-arm-none-eabi gcc-arm-none-eabi
- coqc --version
- ./configure.sh --architecture=armv7 --partition-name=minimal --libpip=/tmp --dx=$LIB/dx --no-command-check
- make minimal.elf
artifacts:
paths:
- minimal.elf
expire_in: 1 hour
test x86 minimal (digger):
stage: test
needs:
- job: build x86 minimal with digger
artifacts: true
script:
- .ci/apt-get.sh qemu-system-x86
- ./configure.sh --architecture=x86 --partition-name=minimal --libpip=/tmp --no-command-check
- make -o minimal.elf test-minimal
test x86 minimal (dx):
stage: test
needs:
- job: build x86 minimal with dx
artifacts: true
script:
- .ci/apt-get.sh qemu-system-x86
- ./configure.sh --architecture=x86 --partition-name=minimal --libpip=/tmp --no-command-check
- make -o minimal.elf test-minimal
test arm minimal (digger):
stage: test
needs:
- job: build arm minimal with digger
artifacts: true
script:
- .ci/apt-get.sh qemu-system-arm
- ./configure.sh --architecture=armv7 --partition-name=minimal --libpip=/tmp --no-command-check
- make -o minimal.elf test-minimal
test arm minimal (dx):
stage: test
needs:
- job: build arm minimal with dx
artifacts: true
script:
- .ci/apt-get.sh qemu-system-arm
- ./configure.sh --architecture=armv7 --partition-name=minimal --libpip=/tmp --no-command-check
- make -o minimal.elf test-minimal
check proofs:
when: manual
needs: []
script:
- coqc --version
- ./configure.sh --architecture=x86 --partition-name=minimal --libpip=/tmp --no-command-check
- make proofs
test x86 nanny_busy_beaver:
stage: test
trigger:
project: 2xs/pip/nanny_busy_beaver
strategy: depend