Admin/isatest/isatest-annomaly
author wenzelm
Sat Oct 04 16:05:09 2008 +0200 (2008-10-04 ago)
changeset 28500 4b79e5d3d0aa
parent 22638 7cea3e27d05f
child 28504 7ad7d7d6df47
permissions -rwxr-xr-x
replaced ISATOOL by ISABELLE_TOOL;
     1 #!/usr/bin/env bash
     2 #
     3 # $Id$
     4 #
     5 # Create AnnoMaLy documentation for Isabelle
     6 #
     7 # Based on http://martin.von-gagern.net/projects/annomaly/
     8 #   2007  Martin von Gagern (martin@von-gagern.net)
     9 
    10 ## global settings
    11 . ~/admin/isatest/isatest-settings
    12 
    13 PRG="$(basename "$0")"
    14 
    15 export SMLNJ_HOME="/home/gagern/annomaly"
    16 export SML_DOC_DIR="$HOME/anno-html"
    17 
    18 ADMIN="$HOME/admin/isatest"
    19 LOGICS="HOL"
    20 
    21 # Abort on any error
    22 set -e -o pipefail
    23 
    24 function usage()
    25 {
    26   echo
    27   echo "Usage: $PRG"
    28   echo
    29   echo "  Generate html documentation from .ML files"
    30   echo
    31   exit 1
    32 }
    33 
    34 function fail()
    35 {
    36   echo "$1" >&2
    37   echo "$(date) $HOSTNAME $PRG: FAILED, $1" >> $MASTERLOG
    38   exit 2
    39 }
    40 
    41 
    42 ## main
    43 
    44 ISABELLE_HOME="$DISTPREFIX/Isabelle"
    45 ISABELLE_TOOL="$ISABELLE_HOME/bin/isatool"
    46 
    47 [ -d $ISABELLE_HOME ] || fail "$ISABELLE_HOME is not a directory."
    48 
    49 
    50 # Create clean output directory
    51 rm -rf "$SML_DOC_DIR"
    52 mkdir "$SML_DOC_DIR"
    53 cp "$SMLNJ_HOME/annomaly/resources/"* "$SML_DOC_DIR"
    54 cat > "$SML_DOC_DIR/.htaccess" <<EOF
    55 DirectoryIndex index.html source.html
    56 <IfModule mod_deflate>
    57 SetOutputFilter DEFLATE 
    58 </IfModule>
    59 AddType text/plain .dot
    60 EOF
    61 
    62 # Prepare build environemnt
    63 cd "$ISABELLE_HOME"
    64 cp "$ADMIN/annomaly.ML" src/Pure/ML-Systems/annomaly.ML
    65 ln -fs run-smlnj lib/scripts/run-annomaly
    66 
    67 cd "$ISABELLE_HOME"
    68 export SML_DOC_REWRITE="isabelle=$(cd src; pwd -P)"
    69 
    70 
    71 # Process image(s)
    72 for L in $LOGICS
    73 do
    74   ( cd "$ISABELLE_HOME/src/$L"; \
    75     cat ~/settings/annomaly >> $ISABELLE_HOME/etc/settings; \
    76     "$ISABELLE_TOOL" make || fail "isabelle make for $L failed." )
    77 done
    78 
    79 
    80 # Postprocess created files
    81 cd "$SML_DOC_DIR"
    82 dot -Tsvg depGraph.dot \
    83   | perl -pe 's/(width|height)="(\d+)/sprintf("%s=\"%.2f",$1,$2*0.6)/ge' \
    84   > depGraph.svg
    85 dot -Tps2 depGraph.dot > depGraph.ps
    86 ps2pdf depGraph.ps depGraph.pdf
    87 
    88 # $ISABELLE_HOME does not seem to occur anywhere ??
    89 # grep -rl "$ISABELLE_HOME" . | xargs sed -i "s@$ISABELLE_HOME@\$ISABELLE_HOME@g"
    90 
    91 
    92 echo "$(date) $HOSTNAME $PRG: annomaly docs generated successfully." >> $MASTERLOG