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