mirror of
https://github.com/AdaCore/SPARKlib.git
synced 2026-02-12 13:11:36 -08:00
23 lines
977 B
Makefile
23 lines
977 B
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)
|