Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

Dangling references and undefined citations are now breaking the document build.
HOL-OCL/Isabelle_DOF/master This commit looks good Details

This commit is contained in:
Achim D. Brucker 2019-04-07 18:07:29 +01:00
parent 40f5fa17d3
commit 0789a96677
1 changed files with 34 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

34
document-generator/document-template/build_lib.sh
View File

@ -129,3 +129,37 @@ $ISABELLE_TOOL latex -o "$OUTFORMAT" "root.tex" && \
$ISABELLE_TOOL latex -o "$OUTFORMAT" "root.tex" && \
$ISABELLE_TOOL latex -o "$OUTFORMAT" "root.tex"
MISSING_CITATIONS=`grep 'Warning.*Citation' root.log | awk '{print $5}' | sort -u`
if [ "$MISSING_CITATIONS" != "" ]; then
echo ""
echo "ERROR (Isabelle/DOF): document referencing inconsistent due to missing citations: "
echo "$MISSING_CITATIONS"
exit 1
fi
DANGLING_REFS=`grep 'Warning.*Refer' root.log | awk '{print $4}' | sort -u`
if [ "$DANGLING_REFS" != "" ]; then
echo ""
echo "ERROR (Isabelle/DOF): document referencing inconsistent due to dangling references:"
echo "$DANGLING_REFS"
echo ""
exit 1
fi
if [ -f "root.blg" ]; then
echo "BibTeX Warnings:"
echo "================"
grep Warning root.blg | sed -e 's/Warning--//'
echo ""
fi
echo "Layout Glitches:"
echo "================"
echo -n "Number of overfull hboxes: "
grep 'Overfull .hbox' root.log | wc -l
echo -n "Number of underfull hboxes: "
grep 'Underfull .hbox' root.log | wc -l
echo -n "Number of overfull vboxes: "
grep 'Overfull .vbox' root.log | wc -l
echo -n "Number of underfull vboxes: "
grep 'Underfull .vbox' root.log | wc -l
echo ""
exit 0