forked from LPCIC/coq-elpi
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Makefile.test.coq.local
31 lines (28 loc) · 1.28 KB
/
Makefile.test.coq.local
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
tests/test_cache_async.vo: COQEXTRAFLAGS=-async-proofs on
tests/test_COQ_ELPI_ATTRIBUTES.vo: export COQ_ELPI_ATTRIBUTES=test=yes,str="some-string"
define test_link
@F="$(1)";\
L1=`grep -n '^p 7\.' $$F | cut -d : -f 1`;\
L2=`grep -n '^p 2\.' $$F | cut -d : -f 1`;\
[ "$$L1" -gt "$$L2" ] || (echo "wrong link order in file $$F"; exit 1);\
for i in `seq 1 10`; do\
N=`grep "^p $$i\\\\." $$F | wc -l`;\
[ "$$N" = "1" ] || (echo "wrong linking: rule p $$i occurs $$N in file $$F"; exit 1);\
done;\
true
endef
post-all:: tests/test_glob.glob
@echo "test coqdoc hyperlinks"
@mkdir -p tests/test_glob/
@N=`coqdoc -d tests/test_glob -R tests elpi.tests tests/test_glob.v 2>&1 | grep -i warning | wc -l`;\
test $$N = 0
@echo "test link order"
@diff -u tests/test_link_order1.txt tests/test_link_order2.txt
@diff -u tests/test_link_order1.txt tests/test_link_order3.txt
@diff -u tests/test_link_order1.txt tests/test_link_order4.txt
@diff -u tests/test_link_order1.txt tests/test_link_order5.txt
@diff -u tests/test_link_order1.txt tests/test_link_order6.txt
@diff -u tests/test_link_order1.txt tests/test_link_order7.txt
@diff -u tests/test_link_order1.txt tests/test_link_order8.txt
@diff -u tests/test_link_order1.txt tests/test_link_order9.txt
$(call test_link, tests/test_link_order1.txt)