Makefile

ALL_CTX=$(wildcard proof/Coq/*.ctx)
ALL_COQ=$(sort $(patsubst %.ctx,%.v,$(ALL_CTX)))

# Do not use cpp with -P switch to remove line directives generated by
# preprocessing, as this also removes blank lines that are needed by
# the Coq printer/parser in Why3 to recognize the VC. Use sed instead to
# remove lines that start with # symbol.
# Also cpp does not understand the sequence slash space end_of_line so we
# added a comment with the first sed. Basically cpp should not be used
# for this but we don't know what to use to replace it. This is a hack.
%.v: %.ctx
	sed -e 's/\\ $$/\\ (\* non escaped EOL for cpp parsing \*)/g' $< | \
sed -e 's/\\$$/\\ (\* non escaped EOL for cpp parsing \*)/g' | \
cpp -w -I proof/Coq/common | sed -e 's/^#.*$$//g' > $@

clean:
	find proof -name "*.v" -delete

check:
	SPARKLIB_INSTALLED=False SPARKLIB_BODY_MODE=On gprbuild -P sparklib_internal.gpr -c -f -gnatc -gnatg -gnat2022 -gnateDSPARK_BODY_MODE=On -gnatwe -k

generate: $(ALL_COQ)