forked from unicoq/unicoq
-
Notifications
You must be signed in to change notification settings - Fork 0
/
.travis.yml
43 lines (40 loc) · 1.27 KB
/
.travis.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
dist: trusty
sudo: required
language: generic
services:
- docker
env:
global:
- NJOBS="2"
- CONTRIB_NAME="unicoq"
matrix:
- COQ_IMAGE="ocaml/opam2:4.05"
install: |
# Prepare the COQ container
docker run -d -i --init --name=COQ -v ${TRAVIS_BUILD_DIR}:/home/coq/${CONTRIB_NAME} -w /home/coq/${CONTRIB_NAME} ${COQ_IMAGE}
docker exec COQ /bin/bash --login -c "
# This bash script is double-quoted to interpolate Travis CI env vars:
echo \"Build triggered by ${TRAVIS_EVENT_TYPE}\"
export PS4='+ \e[33;1m(\$0 @ line \$LINENO) \$\e[0m '
set -ex # -e = exit on failure; -x = trace for debug
opam repo add coq-released https://coq.inria.fr/opam/released
opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev
opam repo list
sudo apt install -y m4
opam install -v -y coq.dev
opam config list
opam repo list
opam list
"
script:
- echo -e "${ANSI_YELLOW}Building ${CONTRIB_NAME}...${ANSI_RESET}" && echo -en 'travis_fold:start:script\\r'
- |
docker exec COQ /bin/bash --login -c "
export PS4='+ \e[33;1m(\$0 @ line \$LINENO) \$\e[0m '
set -ex
sudo chown -R opam:opam /home/coq/${CONTRIB_NAME}
coq_makefile -f Make -o Makefile
make
"
- docker stop COQ # optional
- echo -en 'travis_fold:end:script\\r'