Admin/isatest/isatest-annomaly

tuned proof - no smt call

#!/usr/bin/env bash
#
# Create AnnoMaLy documentation for Isabelle
#
# Based on http://martin.von-gagern.net/projects/annomaly/
#   2007  Martin von Gagern ([e-mail])

## global settings
. ~/admin/isatest/isatest-settings

PRG="$(basename "$0")"

export SMLNJ_HOME="/home/gagern/annomaly"
export SML_DOC_DIR="$HOME/anno-html"

ADMIN="$HOME/admin/isatest"
LOGICS="HOL"

# Abort on any error
set -e -o pipefail

function usage()
{
  echo
  echo "Usage: $PRG"
  echo
  echo "  Generate html documentation from .ML files"
  echo
  exit 1
}

function fail()
{
  echo "$1" >&2
  log "FAILED, $1"
  exit 2
}


## main

ISABELLE_HOME="$DISTPREFIX/Isabelle"
ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle"

[ -d $ISABELLE_HOME ] || fail "$ISABELLE_HOME is not a directory."


# Create clean output directory
rm -rf "$SML_DOC_DIR"
mkdir "$SML_DOC_DIR"
cp "$SMLNJ_HOME/annomaly/resources/"* "$SML_DOC_DIR"
cat > "$SML_DOC_DIR/.htaccess" <<EOF
DirectoryIndex index.html source.html
<IfModule mod_deflate>
SetOutputFilter DEFLATE 
</IfModule>
AddType text/plain .dot
EOF

# Prepare build environemnt
cd "$ISABELLE_HOME"
cp "$ADMIN/annomaly.ML" src/Pure/ML-Systems/annomaly.ML
ln -fs run-smlnj lib/scripts/run-annomaly

cd "$ISABELLE_HOME"
export SML_DOC_REWRITE="isabelle=$(cd src; pwd -P)"


# Process image(s)
for L in $LOGICS
do
  ( cd "$ISABELLE_HOME/src/$L"; \
    cat ~/settings/annomaly >> $ISABELLE_HOME/etc/settings; \
    "$ISABELLE_TOOL" make || fail "isabelle make for $L failed." )
done


# Postprocess created files
cd "$SML_DOC_DIR"
dot -Tsvg depGraph.dot \
  | perl -pe 's/(width|height)="(\d+)/sprintf("%s=\"%.2f",$1,$2*0.6)/ge' \
  > depGraph.svg
dot -Tps2 depGraph.dot > depGraph.ps
ps2pdf depGraph.ps depGraph.pdf

# $ISABELLE_HOME does not seem to occur anywhere ??
# grep -rl "$ISABELLE_HOME" . | xargs sed -i "s@$ISABELLE_HOME@\$ISABELLE_HOME@g"


log "annomaly docs generated successfully."