From 0789a96677c9ecd1cf569137fb1b455e5e220b0a Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Sun, 7 Apr 2019 18:07:29 +0100 Subject: [PATCH] Dangling references and undefined citations are now breaking the document build. --- .../document-template/build_lib.sh | 34 +++++++++++++++++++ 1 file changed, 34 insertions(+) diff --git a/document-generator/document-template/build_lib.sh b/document-generator/document-template/build_lib.sh index 64376b7..119b1a0 100755 --- a/document-generator/document-template/build_lib.sh +++ b/document-generator/document-template/build_lib.sh @@ -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