Commit 8d6b42b6 authored by Felipe Cerqueira's avatar Felipe Cerqueira
Browse files

Fix 'make validate' name clashes

parent 835fdffb
......@@ -52,7 +52,7 @@ COQDOCLIBS?=-R . rt
COQDEP?=$(COQBIN)coqdep -c
COQCHKFLAGS?=-silent -o
COQDOCFLAGS?=-interpolate -utf8
......@@ -207,7 +207,7 @@ all-gal.pdf: $(VFILES)
$(COQDOC) -toc $(COQDOCFLAGS) -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
validate: $(VOFILES)
$(COQCHK) $(COQCHKFLAGS) $(COQLIBS) $(notdir $(^:.vo=))
$(COQCHK) $(COQCHKFLAGS) $(COQLIBS) $(addprefix rt., $(subst /,., $(^:.vo=)))
beautify: $(VFILES:=.beautified)
for file in $^; do mv $${file%.beautified} $${file%beautified}old && mv $${file} $${file%.beautified}; done
# Compile all *.v files (except the ones that define the decidable equality). Those
# are directly included in other files.
coq_makefile -R . rt $(find -name "*.v" ! -name "*#*" ! -name "*eqdec*.v" -print) -o Makefile
# Fix the 'make validate' command. It doesn't handle the library prefix properly
# and cause clashes for files with the same name. This forces full filenames and
# adds the rt. prefix
sed -i 's|$(notdir $(^:.vo=))|$(addprefix rt., $(subst /,., $(^:.vo=)))|g' Makefile
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment