1.1 --- a/Admin/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,98 +0,0 @@
1.4 -#!/bin/sh
1.5 -
1.6 -# Create AnnoMaLy documentation for Isabelle
1.7 -# See http://martin.von-gagern.net/projects/annomaly/
1.8 -# 2007 Martin von Gagern (martin@von-gagern.net)
1.9 -
1.10 -# Abort on any error
1.11 -set -e -o pipefail
1.12 -
1.13 -BUILD_DIR="$HOME/isabelle.annomaly"
1.14 -ISABELLE_HOME="$BUILD_DIR/Isabelle"
1.15 -ISABELLE_CVS="$HOME/isabelle.cvs"
1.16 -ADMIN_CVS="$ISABELLE_CVS/Admin"
1.17 -# ISABELLE_HOME="$ISABELLE_CVS/Distribution"
1.18 -ISABELLE_SRC="$ISABELLE_HOME/src"
1.19 -HTML_DIR="$HOME/html-data/isabelle-doc"
1.20 -export CVS_RSH=ssh
1.21 -export SMLNJ_HOME="$HOME/annomaly"
1.22 -export PATH="$SMLNJ_HOME/bin:$PATH"
1.23 -export SML_DOC_DIR="$HTML_DIR.tmp"
1.24 -# export SML_DOC_DEBUG="all"
1.25 -TARGET=HOL
1.26 -CVSUP=true
1.27 -
1.28 -# Parse command line
1.29 -for ARG in "$@"; do case "$ARG" in
1.30 - -p) TARGET=Pure ;;
1.31 - -n) CVSUP=false ;;
1.32 - -l) export SML_LOG_DIR="$HOME/logs" ;;
1.33 -esac; done
1.34 -
1.35 -# Update CVS
1.36 -cd "$ADMIN_CVS"
1.37 -if $CVSUP; then
1.38 - echo "Updating CVS"
1.39 - cvs -q up -d
1.40 -fi
1.41 -
1.42 -# Find nightly isabelle tarball
1.43 -ISABELLE_TAR=""
1.44 -for i in /home/html/isatest/Isabelle_[0-9]*-20[0-9][0-9].tar.gz; do
1.45 - if [[ -r "$i" ]]; then ISABELLE_TAR="$i"; fi
1.46 -done
1.47 -if [[ -z $ISABELLE_TAR ]]; then
1.48 - echo "No isabelle tarball found!" >&2
1.49 - exit 1
1.50 -fi
1.51 -
1.52 -# Create build environemnt
1.53 -mkdir -p "$BUILD_DIR"
1.54 -cd "$BUILD_DIR"
1.55 -if [[ -d Isabelle ]]; then
1.56 - rm -rf *
1.57 -fi
1.58 -tar xzf "$ISABELLE_TAR"
1.59 -cd "$ISABELLE_HOME"
1.60 -cp "$ADMIN_CVS"/isatest/annomaly.ML src/Pure/ML-Systems/annomaly.ML
1.61 -ln -s run-smlnj lib/scripts/run-annomaly
1.62 -
1.63 -# Create clean output directory
1.64 -rm -rf "$SML_DOC_DIR"
1.65 -mkdir "$SML_DOC_DIR"
1.66 -cp "$SMLNJ_HOME/annomaly/resources/"* "$SML_DOC_DIR"
1.67 -cat > "$SML_DOC_DIR/.htaccess" <<EOF
1.68 -DirectoryIndex index.html source.html
1.69 -<IfModule mod_deflate>
1.70 -SetOutputFilter DEFLATE
1.71 -</IfModule>
1.72 -AddType text/plain .dot
1.73 -EOF
1.74 -
1.75 -# Build isabelle
1.76 -ISABELLE_HOME="$(cd "$ISABELLE_HOME"; pwd -P)"
1.77 -cd "$ISABELLE_HOME"
1.78 -export SML_DOC_REWRITE="isabelle=$(cd src; pwd -P)"
1.79 -rm -rf heaps
1.80 -./build -b $TARGET
1.81 -cd "$BUILD_DIR"
1.82 -rm -rf *
1.83 -
1.84 -# Postprocess created files
1.85 -cd $SML_DOC_DIR
1.86 -dot -Tsvg depGraph.dot \
1.87 - | perl -pe 's/(width|height)="(\d+)/sprintf("%s=\"%.2f",$1,$2*0.6)/ge' \
1.88 - > depGraph.svg
1.89 -dot -Tps2 depGraph.dot > depGraph.ps
1.90 -ps2pdf depGraph.ps depGraph.pdf
1.91 -grep -rl "$ISABELLE_HOME" . | xargs sed -i "s@$ISABELLE_HOME@\$ISABELLE_HOME@g"
1.92 -
1.93 -# Install result by renaming, to be almost atomic
1.94 -rm -rf "$HTML_DIR.bac"
1.95 -if [[ -d $HTML_DIR ]]; then mv "$HTML_DIR" "$HTML_DIR.bac"; fi
1.96 -mv "$SML_DOC_DIR" "$HTML_DIR"
1.97 -rm -rf "$HTML_DIR.bac"
1.98 -
1.99 -# Done
1.100 -echo "Completed successfully"
1.101 -exit 0
2.1 --- a/Admin/isatest/annomaly.ML Mon Jul 23 12:05:48 2012 +0200
2.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
2.3 @@ -1,69 +0,0 @@
2.4 -(* Title: Admin/isatest/annomaly.ML
2.5 - Author: Martin von Gagern <martin@von-gagern.net>
2.6 -*)
2.7 -
2.8 -use "ML-Systems/smlnj.ML";
2.9 -
2.10 -local
2.11 -
2.12 - val smlnj_use_text = use_text
2.13 -
2.14 - val smlnj_use_file = use_file
2.15 -
2.16 - val smlnj_forget_structure = forget_structure
2.17 -
2.18 - fun mkAbsolute path =
2.19 - OS.Path.mkAbsolute { path = path, relativeTo = OS.FileSys.getDir () }
2.20 -
2.21 - fun toArcs path = #arcs (OS.Path.fromString path)
2.22 -
2.23 - val isabelleHome =
2.24 - case OS.Process.getEnv "ISABELLE_HOME"
2.25 - of NONE => OS.FileSys.getDir ()
2.26 - | SOME home => mkAbsolute home
2.27 -
2.28 - fun noparent [] = []
2.29 - | noparent (n :: ns) =
2.30 - if n = OS.Path.parentArc then noparent ns else n :: noparent ns
2.31 -
2.32 - fun isabellePath [] = []
2.33 - | isabellePath ("src" :: name) = "Isabelle" :: name
2.34 - | isabellePath (name as (n :: ns)) =
2.35 - if n = OS.Path.parentArc then noparent ns else "Isabelle" :: name
2.36 -
2.37 - fun rewrite defPrefix name =
2.38 - let val abs = mkAbsolute name
2.39 - val rel = OS.Path.mkRelative { path = abs, relativeTo = isabelleHome }
2.40 - val exists = (OS.FileSys.access(abs, nil)
2.41 - handle OS.SysErr _ => false)
2.42 - in if exists andalso rel <> ""
2.43 - then isabellePath (toArcs rel)
2.44 - else defPrefix @ noparent (toArcs name)
2.45 - end handle OS.Path.Path => defPrefix @ noparent (toArcs name)
2.46 -
2.47 -in
2.48 -
2.49 - fun use_text tune str_of_pos name_space (line, name) p v t =
2.50 - let val name = case name of "" => "unnamed" | name => name
2.51 - val arcs = rewrite ["use_text"] name
2.52 - (* should we have different files for different line numbers? *
2.53 - val arcs = if line <= 1 then arcs
2.54 - else arcs @ [ "l." ^ Int.toString line ]
2.55 - *)
2.56 - val arcs = if t = "structure Isabelle =\nstruct\nend;"
2.57 - andalso name = "ML"
2.58 - then ["empty_Isabelle", "empty" ] else arcs
2.59 - val _ = AnnoMaLy.nameNextStream arcs
2.60 - in smlnj_use_text tune str_of_pos name_space (line, name) p v t end;
2.61 -
2.62 - fun use_file tune str_of_pos name_space output verbose name =
2.63 - let val arcs = rewrite ["use_file"] name
2.64 - val _ = AnnoMaLy.nameNextStream arcs
2.65 - in smlnj_use_file tune str_of_pos name_space output verbose name end;
2.66 -
2.67 - fun forget_structure name =
2.68 - let val arcs = [ "forget_structure", name ]
2.69 - val _ = AnnoMaLy.nameNextStream arcs
2.70 - in smlnj_forget_structure name end;
2.71 -
2.72 -end;
3.1 --- a/Admin/isatest/isatest-annomaly Mon Jul 23 12:05:48 2012 +0200
3.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
3.3 @@ -1,90 +0,0 @@
3.4 -#!/usr/bin/env bash
3.5 -#
3.6 -# Create AnnoMaLy documentation for Isabelle
3.7 -#
3.8 -# Based on http://martin.von-gagern.net/projects/annomaly/
3.9 -# 2007 Martin von Gagern (martin@von-gagern.net)
3.10 -
3.11 -## global settings
3.12 -. ~/admin/isatest/isatest-settings
3.13 -
3.14 -PRG="$(basename "$0")"
3.15 -
3.16 -export SMLNJ_HOME="/home/gagern/annomaly"
3.17 -export SML_DOC_DIR="$HOME/anno-html"
3.18 -
3.19 -ADMIN="$HOME/admin/isatest"
3.20 -LOGICS="HOL"
3.21 -
3.22 -# Abort on any error
3.23 -set -e -o pipefail
3.24 -
3.25 -function usage()
3.26 -{
3.27 - echo
3.28 - echo "Usage: $PRG"
3.29 - echo
3.30 - echo " Generate html documentation from .ML files"
3.31 - echo
3.32 - exit 1
3.33 -}
3.34 -
3.35 -function fail()
3.36 -{
3.37 - echo "$1" >&2
3.38 - log "FAILED, $1"
3.39 - exit 2
3.40 -}
3.41 -
3.42 -
3.43 -## main
3.44 -
3.45 -ISABELLE_HOME="$DISTPREFIX/Isabelle"
3.46 -ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle"
3.47 -
3.48 -[ -d $ISABELLE_HOME ] || fail "$ISABELLE_HOME is not a directory."
3.49 -
3.50 -
3.51 -# Create clean output directory
3.52 -rm -rf "$SML_DOC_DIR"
3.53 -mkdir "$SML_DOC_DIR"
3.54 -cp "$SMLNJ_HOME/annomaly/resources/"* "$SML_DOC_DIR"
3.55 -cat > "$SML_DOC_DIR/.htaccess" <<EOF
3.56 -DirectoryIndex index.html source.html
3.57 -<IfModule mod_deflate>
3.58 -SetOutputFilter DEFLATE
3.59 -</IfModule>
3.60 -AddType text/plain .dot
3.61 -EOF
3.62 -
3.63 -# Prepare build environemnt
3.64 -cd "$ISABELLE_HOME"
3.65 -cp "$ADMIN/annomaly.ML" src/Pure/ML-Systems/annomaly.ML
3.66 -ln -fs run-smlnj lib/scripts/run-annomaly
3.67 -
3.68 -cd "$ISABELLE_HOME"
3.69 -export SML_DOC_REWRITE="isabelle=$(cd src; pwd -P)"
3.70 -
3.71 -
3.72 -# Process image(s)
3.73 -for L in $LOGICS
3.74 -do
3.75 - ( cd "$ISABELLE_HOME/src/$L"; \
3.76 - cat ~/settings/annomaly >> $ISABELLE_HOME/etc/settings; \
3.77 - "$ISABELLE_TOOL" make || fail "isabelle make for $L failed." )
3.78 -done
3.79 -
3.80 -
3.81 -# Postprocess created files
3.82 -cd "$SML_DOC_DIR"
3.83 -dot -Tsvg depGraph.dot \
3.84 - | perl -pe 's/(width|height)="(\d+)/sprintf("%s=\"%.2f",$1,$2*0.6)/ge' \
3.85 - > depGraph.svg
3.86 -dot -Tps2 depGraph.dot > depGraph.ps
3.87 -ps2pdf depGraph.ps depGraph.pdf
3.88 -
3.89 -# $ISABELLE_HOME does not seem to occur anywhere ??
3.90 -# grep -rl "$ISABELLE_HOME" . | xargs sed -i "s@$ISABELLE_HOME@\$ISABELLE_HOME@g"
3.91 -
3.92 -
3.93 -log "annomaly docs generated successfully."
4.1 --- a/Admin/isatest/settings/annomaly Mon Jul 23 12:05:48 2012 +0200
4.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
4.3 @@ -1,26 +0,0 @@
4.4 -# -*- shell-script -*- :mode=shellscript:
4.5 -
4.6 -ML_SYSTEM=annomaly
4.7 -ML_HOME="$SMLNJ_HOME/bin"
4.8 -ML_OPTIONS="-m $SMLNJ_HOME/annomaly/annomaly.cm @SMLdebug=/dev/null"
4.9 -ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
4.10 -
4.11 -
4.12 -ISABELLE_HOME_USER="$HOME/isabelle-annomaly"
4.13 -
4.14 -# Where to look for isabelle tools (multiple dirs separated by ':').
4.15 -ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
4.16 -
4.17 -# Location for temporary files (should be on a local file system).
4.18 -ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
4.19 -
4.20 -
4.21 -# Heap input locations. ML system identifier is included in lookup.
4.22 -ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
4.23 -
4.24 -# Heap output location. ML system identifier is appended automatically later on.
4.25 -ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
4.26 -ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
4.27 -
4.28 -ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true"
4.29 -