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
|
COQ_MINOR=$(shell echo $(COQ_VERSION) | cut -d . -f 2 | cut -d + -f 1)
output_for=`\
if [ -e $(1).out.$(COQ_MINOR) ]; then\
echo $(1).out.$(COQ_MINOR);\
else\
echo $(1).out;\
fi`
DIFF=\
@if [ -z "$$COQ_ELPI_ATTRIBUTES" ]; then \
echo OUTPUT DIFF $(1);\
$(COQTOP) $(COQFLAGS) $(COQLIBS) -topfile $(1) \
< $(1) 2>&1 \
| sed 's/Coq < *//g' \
| sed 's/Rocq < *//g' \
| grep -v '^$$' \
| grep -v -e "Skipping rcfile" -e "is declared" -e "is defined" -e "Loading ML file" -e "Welcome to Coq" -e "Welcome to Rocq" \
| sed 's/characters \([0-9]\+\)-[0-9]\+/character \1/' \
> $(1).out.aux;\
diff -u --strip-trailing-cr $(call output_for,$(1)) $(1).out.aux;\
fi
post-all::
$(call DIFF, tests/err_missin_subject.v)
$(call DIFF, tests/compress_coe.v)
$(call DIFF, tests/about.v)
$(call DIFF, tests/howto.v)
$(call DIFF, tests/err_miss_key.v)
$(call DIFF, tests/missing_join_error.v)
$(call DIFF, tests/not_same_key.v)
$(call DIFF, tests/hnf.v)
$(call DIFF, tests/err_miss_dep.v)
$(call DIFF, tests/err_bad_mix.v)
$(call DIFF, tests/err_instance_nop.v)
|
