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