Admin/isatest/isatest-annomaly
changeset 49459 c8c7b2b388d1
parent 49458 6f2762eedca0
child 49460 cb4136e4cabf
     1.1 --- a/Admin/isatest/isatest-annomaly	Mon Jul 23 12:05:48 2012 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,90 +0,0 @@
     1.4 -#!/usr/bin/env bash
     1.5 -#
     1.6 -# Create AnnoMaLy documentation for Isabelle
     1.7 -#
     1.8 -# Based on http://martin.von-gagern.net/projects/annomaly/
     1.9 -#   2007  Martin von Gagern (martin@von-gagern.net)
    1.10 -
    1.11 -## global settings
    1.12 -. ~/admin/isatest/isatest-settings
    1.13 -
    1.14 -PRG="$(basename "$0")"
    1.15 -
    1.16 -export SMLNJ_HOME="/home/gagern/annomaly"
    1.17 -export SML_DOC_DIR="$HOME/anno-html"
    1.18 -
    1.19 -ADMIN="$HOME/admin/isatest"
    1.20 -LOGICS="HOL"
    1.21 -
    1.22 -# Abort on any error
    1.23 -set -e -o pipefail
    1.24 -
    1.25 -function usage()
    1.26 -{
    1.27 -  echo
    1.28 -  echo "Usage: $PRG"
    1.29 -  echo
    1.30 -  echo "  Generate html documentation from .ML files"
    1.31 -  echo
    1.32 -  exit 1
    1.33 -}
    1.34 -
    1.35 -function fail()
    1.36 -{
    1.37 -  echo "$1" >&2
    1.38 -  log "FAILED, $1"
    1.39 -  exit 2
    1.40 -}
    1.41 -
    1.42 -
    1.43 -## main
    1.44 -
    1.45 -ISABELLE_HOME="$DISTPREFIX/Isabelle"
    1.46 -ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle"
    1.47 -
    1.48 -[ -d $ISABELLE_HOME ] || fail "$ISABELLE_HOME is not a directory."
    1.49 -
    1.50 -
    1.51 -# Create clean output directory
    1.52 -rm -rf "$SML_DOC_DIR"
    1.53 -mkdir "$SML_DOC_DIR"
    1.54 -cp "$SMLNJ_HOME/annomaly/resources/"* "$SML_DOC_DIR"
    1.55 -cat > "$SML_DOC_DIR/.htaccess" <<EOF
    1.56 -DirectoryIndex index.html source.html
    1.57 -<IfModule mod_deflate>
    1.58 -SetOutputFilter DEFLATE 
    1.59 -</IfModule>
    1.60 -AddType text/plain .dot
    1.61 -EOF
    1.62 -
    1.63 -# Prepare build environemnt
    1.64 -cd "$ISABELLE_HOME"
    1.65 -cp "$ADMIN/annomaly.ML" src/Pure/ML-Systems/annomaly.ML
    1.66 -ln -fs run-smlnj lib/scripts/run-annomaly
    1.67 -
    1.68 -cd "$ISABELLE_HOME"
    1.69 -export SML_DOC_REWRITE="isabelle=$(cd src; pwd -P)"
    1.70 -
    1.71 -
    1.72 -# Process image(s)
    1.73 -for L in $LOGICS
    1.74 -do
    1.75 -  ( cd "$ISABELLE_HOME/src/$L"; \
    1.76 -    cat ~/settings/annomaly >> $ISABELLE_HOME/etc/settings; \
    1.77 -    "$ISABELLE_TOOL" make || fail "isabelle make for $L failed." )
    1.78 -done
    1.79 -
    1.80 -
    1.81 -# Postprocess created files
    1.82 -cd "$SML_DOC_DIR"
    1.83 -dot -Tsvg depGraph.dot \
    1.84 -  | perl -pe 's/(width|height)="(\d+)/sprintf("%s=\"%.2f",$1,$2*0.6)/ge' \
    1.85 -  > depGraph.svg
    1.86 -dot -Tps2 depGraph.dot > depGraph.ps
    1.87 -ps2pdf depGraph.ps depGraph.pdf
    1.88 -
    1.89 -# $ISABELLE_HOME does not seem to occur anywhere ??
    1.90 -# grep -rl "$ISABELLE_HOME" . | xargs sed -i "s@$ISABELLE_HOME@\$ISABELLE_HOME@g"
    1.91 -
    1.92 -
    1.93 -log "annomaly docs generated successfully."