mirror of
https://github.com/AdaCore/SPARKlib.git
synced 2026-02-12 13:11:36 -08:00
7eee48d617
This patch copies and adapts the source files of SPARKlib from the spark2014 repository into this one. It also changes the license of these files, as SPARKlib is now licensed under Apache 2.0.
20 lines
820 B
Makefile
20 lines
820 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
|
|
|
|
generate: $(ALL_COQ)
|