Admin/isatest/annomaly

Rewrite the Probability theory.

Introduced pinfreal as real numbers with infinity.
Use pinfreal as value for measures.
Introduces Lebesgue Measure based on the integral in Multivariate Analysis.
Proved Radon Nikodym for arbitrary sigma finite measure spaces.

#!/bin/sh

# Create AnnoMaLy documentation for Isabelle
# See http://martin.von-gagern.net/projects/annomaly/
#   2007  Martin von Gagern ([e-mail])

# Abort on any error
set -e -o pipefail

BUILD_DIR="$HOME/isabelle.annomaly"
ISABELLE_HOME="$BUILD_DIR/Isabelle"
ISABELLE_CVS="$HOME/isabelle.cvs"
ADMIN_CVS="$ISABELLE_CVS/Admin"
# ISABELLE_HOME="$ISABELLE_CVS/Distribution"
ISABELLE_SRC="$ISABELLE_HOME/src"
HTML_DIR="$HOME/html-data/isabelle-doc"
export CVS_RSH=ssh
export SMLNJ_HOME="$HOME/annomaly"
export PATH="$SMLNJ_HOME/bin:$PATH"
export SML_DOC_DIR="$HTML_DIR.tmp"
# export SML_DOC_DEBUG="all"
TARGET=HOL
CVSUP=true

# Parse command line
for ARG in "$@"; do case "$ARG" in
	-p) TARGET=Pure ;;
	-n) CVSUP=false ;;
	-l) export SML_LOG_DIR="$HOME/logs" ;;
esac; done

# Update CVS
cd "$ADMIN_CVS"
if $CVSUP; then
  echo "Updating CVS"
  cvs -q up -d
fi

# Find nightly isabelle tarball
ISABELLE_TAR=""
for i in /home/html/isatest/Isabelle_[0-9]*-20[0-9][0-9].tar.gz; do
  if [[ -r "$i" ]]; then ISABELLE_TAR="$i"; fi
done
if [[ -z $ISABELLE_TAR ]]; then
  echo "No isabelle tarball found!" >&2
  exit 1
fi

# Create build environemnt
mkdir -p "$BUILD_DIR"
cd "$BUILD_DIR"
if [[ -d Isabelle ]]; then
  rm -rf *
fi
tar xzf "$ISABELLE_TAR"
cd "$ISABELLE_HOME"
cp "$ADMIN_CVS"/isatest/annomaly.ML src/Pure/ML-Systems/annomaly.ML
ln -s run-smlnj lib/scripts/run-annomaly

# 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

# Build isabelle
ISABELLE_HOME="$(cd "$ISABELLE_HOME"; pwd -P)"
cd "$ISABELLE_HOME"
export SML_DOC_REWRITE="isabelle=$(cd src; pwd -P)"
rm -rf heaps
./build -b $TARGET
cd "$BUILD_DIR"
rm -rf *

# 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
grep -rl "$ISABELLE_HOME" . | xargs sed -i "s@$ISABELLE_HOME@\$ISABELLE_HOME@g"

# Install result by renaming, to be almost atomic
rm -rf "$HTML_DIR.bac"
if [[ -d $HTML_DIR ]]; then mv "$HTML_DIR" "$HTML_DIR.bac"; fi
mv "$SML_DOC_DIR" "$HTML_DIR"
rm -rf "$HTML_DIR.bac"

# Done
echo "Completed successfully"
exit 0