Admin/isatest/isatest-annomaly
author haftmann
Thu, 18 Nov 2010 17:01:15 +0100
changeset 40602 91e583511113
parent 31582 4753c317d5c1
permissions -rwxr-xr-x
map_fun combinator in theory Fun
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
# Create AnnoMaLy documentation for Isabelle
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
# 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
     6
#   2007  Martin von Gagern (martin@von-gagern.net)
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
     7
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
     8
## global settings
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
     9
. ~/admin/isatest/isatest-settings
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    10
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    11
PRG="$(basename "$0")"
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
export SMLNJ_HOME="/home/gagern/annomaly"
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    14
export SML_DOC_DIR="$HOME/anno-html"
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    15
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    16
ADMIN="$HOME/admin/isatest"
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    17
LOGICS="HOL"
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    18
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    19
# Abort on any error
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    20
set -e -o pipefail
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    21
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    22
function usage()
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
  echo
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    25
  echo "Usage: $PRG"
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 "  Generate html documentation from .ML files"
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
  exit 1
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    30
}
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    31
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    32
function fail()
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
  echo "$1" >&2
28539
bdb308737bfd do logging to MASTERLOG centrally (avoid multiple writers over NFS as
kleing
parents: 28504
diff changeset
    35
  log "FAILED, $1"
22638
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    36
  exit 2
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    37
}
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    38
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
## main
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
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
    43
ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle"
22638
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    44
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    45
[ -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
    46
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    47
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    48
# Create clean output directory
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    49
rm -rf "$SML_DOC_DIR"
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    50
mkdir "$SML_DOC_DIR"
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    51
cp "$SMLNJ_HOME/annomaly/resources/"* "$SML_DOC_DIR"
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    52
cat > "$SML_DOC_DIR/.htaccess" <<EOF
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    53
DirectoryIndex index.html source.html
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    54
<IfModule mod_deflate>
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    55
SetOutputFilter DEFLATE 
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    56
</IfModule>
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    57
AddType text/plain .dot
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    58
EOF
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    59
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    60
# Prepare build environemnt
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    61
cd "$ISABELLE_HOME"
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    62
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
    63
ln -fs run-smlnj lib/scripts/run-annomaly
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    64
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    65
cd "$ISABELLE_HOME"
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    66
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
    67
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    68
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    69
# Process image(s)
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    70
for L in $LOGICS
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    71
do
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    72
  ( cd "$ISABELLE_HOME/src/$L"; \
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    73
    cat ~/settings/annomaly >> $ISABELLE_HOME/etc/settings; \
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 22638
diff changeset
    74
    "$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
    75
done
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    76
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    77
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    78
# Postprocess created files
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    79
cd "$SML_DOC_DIR"
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    80
dot -Tsvg depGraph.dot \
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    81
  | 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
    82
  > depGraph.svg
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    83
dot -Tps2 depGraph.dot > depGraph.ps
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    84
ps2pdf depGraph.ps depGraph.pdf
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    85
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    86
# $ISABELLE_HOME does not seem to occur anywhere ??
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    87
# 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
    88
7cea3e27d05f isatest version of annomaly script. to be run from istatest-makedist.
kleing
parents:
diff changeset
    89
28539
bdb308737bfd do logging to MASTERLOG centrally (avoid multiple writers over NFS as
kleing
parents: 28504
diff changeset
    90
log "annomaly docs generated successfully."