create_makefile.sh 2.06 KB
Newer Older
1 2 3 4 5 6 7 8 9 10
#!/bin/bash 

# Include rt-proofs library in _CoqProject. (For Coq versions >= 8.6, remove spurious warnings.)
version=$(echo $(coqc -v 1) | grep -o "version .\.." | tail -c 4)
if ([ "$version" == "8.4" ] || [ "$version" == "8.5" ]) then
  echo "-R . rt" > _CoqProject
else
  echo -R . rt -arg \"-w -notation-overriden,-parsing\" > _CoqProject
fi

11 12
# Compile all *.v files (except the ones that define the decidable equality). Those
# are directly included in other files.
13
coq_makefile -f _CoqProject $(find . -name "*.v" ! -name "*#*" ! -name "*eqdec*.v" -print) -o Makefile
14 15 16 17

# 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
18 19
if [ "$(uname)" == "Darwin" ]; then
	sed -i '' 's|$(notdir $(^:.vo=))|$(addprefix rt., $(subst /,., $(^:.vo=)))|g' Makefile
20
else
21 22 23
	sed -i 's|$(notdir $(^:.vo=))|$(addprefix rt., $(subst /,., $(^:.vo=)))|g' Makefile
fi

24 25

# Fix 'make html' so that it parses comments and has links to ssreflect.
26 27
if [ "$(uname)" == "Darwin" ]; then
	sed -i '' 's|-interpolate -utf8|-interpolate -utf8 --plain-comments --parse-comments --external https://math-comp.github.io/math-comp/htmldoc/ mathcomp|g' Makefile
28
else
29 30
	sed -i 's|-interpolate -utf8|-interpolate -utf8 --plain-comments --parse-comments --external https://math-comp.github.io/math-comp/htmldoc/ mathcomp|g' Makefile
fi
31

32
# Fix 'make clean' to remove all binary files, regardless of name
33 34
if [ "$(uname)" == "Darwin" ]; then
	sed -i '' 's|rm -f $(VOFILES) $(VOFILES:.vo=.vio) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old)|find . -name "*.vo" -delete -o -name "*.glob" -delete -o -name "*.v.d" -delete -o -name "*.vio" -delete -o -name "*.old" -delete -o -name "*.beautified" -delete|g' Makefile
35
else
36 37 38
	sed -i 's|rm -f $(VOFILES) $(VOFILES:.vo=.vio) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old)|find . -name "*.vo" -delete -o -name "*.glob" -delete -o -name "*.v.d" -delete -o -name "*.vio" -delete -o -name "*.old" -delete -o -name "*.beautified" -delete|g' Makefile
fi