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

# -gnatwU is needed because the only use some units make of SPARK.Body_Mode is
# in a SPARK_Mode pragma or aspect, and the front end does not record that as a
# reference, so -gnatg would report the with clause as unused.
# ??? Drop it once the front end records such references.
CHECK_SWITCHES=-c -f -gnatc -gnatg -gnatwU -gnat2022 -gnatwe -k

# Both libraries are checked in the default mode, and the full one is checked
# in body mode as well.
# We don't check light library in body mode due to a front-end crash:
#   eng/toolchain/gnat#2015
check:
	SPARKLIB_INSTALLED=False gprbuild -P sparklib_internal.gpr $(CHECK_SWITCHES)
	SPARKLIB_INSTALLED=False gprbuild -P sparklib_light_internal.gpr $(CHECK_SWITCHES)
	SPARKLIB_INSTALLED=False SPARKLIB_BODY_MODE=On gprbuild -P sparklib_internal.gpr $(CHECK_SWITCHES)

format:
	SPARKLIB_INSTALLED=False gnatformat -P sparklib_internal.gpr
	SPARKLIB_INSTALLED=False gnatformat -P sparklib_light_internal.gpr

generate: $(ALL_COQ)