aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.ci
blob: 1b09905cc76f37839520613aae0473c786f702b9 (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
CI_TARGETS=ci-all \
    ci-bignums \
    ci-color \
    ci-compcert \
    ci-coq-dpdgraph \
    ci-coquelicot \
    ci-cpdt \
    ci-fiat-crypto \
    ci-fiat-parsers \
    ci-flocq \
    ci-formal-topology \
    ci-geocoq \
    ci-hott \
    ci-iris-coq \
    ci-math-classes \
    ci-math-comp \
    ci-metacoq \
    ci-sf \
    ci-tlc \
    ci-unimath \
    ci-vst

.PHONY: $(CI_TARGETS)

# Generic rule, we use make to easy travis integraton with mixed rules
$(CI_TARGETS): ci-%:
	rm -f ci-$*.ok
	+(./dev/ci/ci-$*.sh 2>&1 && touch ci-$*.ok) | tee time-of-build.log
	echo 'Aggregating timing log...' && echo -en 'travis_fold:start:coq.test.timing\\r'
	python ./tools/make-one-time-file.py time-of-build.log
	echo -en 'travis_fold:end:coq.test.timing\\r'
	rm ci-$*.ok # must not be -f; we're checking to see that it exists