Makefile.test-suite.coq.local

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/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)