Skip to content
Snippets Groups Projects
Commit e5a110b0 authored by Björn Brandenburg's avatar Björn Brandenburg
Browse files

update create_makefile.sh to patch up coqdoc.css

...while at it, remove some old cruft in there.
parent 1bc558a8
No related branches found
No related tags found
No related merge requests found
#!/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
# Include rt-proofs library in _CoqProject.
# (For Coq versions >= 8.6, remove spurious warnings.)
echo -R . rt -arg \"-w -notation-overriden,-parsing\" > _CoqProject
# Compile all *.v files (except the ones that define the decidable equality). Those
# are directly included in other files.
coq_makefile -f _CoqProject $(find . -name "*.v" ! -name "*#*" ! -name "*eqdec*.v" ! -path "./.git/*" -print) -o Makefile
# Compile all *.v files
coq_makefile -f _CoqProject $(find . -name "*.v" ! -name "*#*" ! -path "./.git/*" -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
......@@ -24,17 +19,13 @@ fi
# Fix 'make html' so that it parses comments and has links to ssreflect.
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
sed -i '' 's|-interpolate -utf8|--interpolate --utf8 --plain-comments --parse-comments --external https://math-comp.github.io/math-comp/htmldoc/ mathcomp|g' Makefile
else
sed -i 's|-interpolate -utf8|-interpolate -utf8 --plain-comments --parse-comments --external https://math-comp.github.io/math-comp/htmldoc/ mathcomp|g' Makefile
fi
# Fix 'make clean' to remove all binary files, regardless of name
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
else
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
sed -i 's|-interpolate -utf8|--interpolate --utf8 --plain-comments --parse-comments --external https://math-comp.github.io/math-comp/htmldoc/ mathcomp|g' Makefile
fi
# Patch Makefile.coqdocjs for pretty documentation targets
printf "\n# Include pretty documentation targets\ninclude scripts/coqdocjs/Makefile.coqdocjs" >> Makefile
# Patch HTML target to switch out color
patch -s < scripts/Makefile.patch
--- Makefile.orig 2019-10-15 22:37:51.000000000 +0200
+++ Makefile 2019-10-15 22:33:50.000000000 +0200
@@ -422,6 +422,9 @@
$(HIDE)mkdir -p html
$(HIDE)$(COQDOC) \
-toc $(COQDOCFLAGS) -html $(GAL) $(COQDOCLIBS) -d html $(VFILES)
+# Prosa hack: let's tweak the style a bit
+ $(HIDE)sed -i.bak "s/#90bdff/#eeeeee/" html/coqdoc.css
+ $(HIDE)rm html/coqdoc.css.bak
mlihtml: $(MLIFILES:.mli=.cmi)
$(SHOW)'CAMLDOC -d $@'
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment