Admin/isatest/isatest-annomaly
author bulwahn
Thu, 07 Jul 2011 23:33:14 +0200
changeset 43704 47b0be18ccbe
parent 31582 4753c317d5c1
permissions -rwxr-xr-x
floor and ceiling definitions are not code equations -- this enables trivial evaluation of floor and ceiling

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

## 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."