Changed AnnoMaLy build process from CVS to tarball sources.
Moved annomaly.ML from the official sources to the isatest directory.
--- a/Admin/isatest/annomaly Tue Mar 20 17:07:23 2007 +0100
+++ b/Admin/isatest/annomaly Tue Mar 20 20:42:14 2007 +0100
@@ -7,14 +7,17 @@
# Abort on any error
set -e -o pipefail
-ISABELLE_CVS="$(cd "$HOME/isabelle.cvs"; pwd -P)"
-ISABELLE_HOME="$ISABELLE_CVS/Distribution"
+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_REWRITE="isabelle=$ISABELLE_CVS"
# export SML_DOC_DEBUG="all"
TARGET=HOL
CVSUP=true
@@ -26,6 +29,34 @@
-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"
@@ -38,17 +69,14 @@
AddType text/plain .dot
EOF
-# Update CVS
-cd "$ISABELLE_CVS"
-if $CVSUP; then
- echo "Updating CVS"
- cvs -q up -d
-fi
-
# Build isabelle
+ISABELLE_HOME="$(cd "$ISABELLE_HOME"; pwd -P)"
cd "$ISABELLE_HOME"
-rm -rf heaps/*
+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
@@ -59,7 +87,7 @@
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
+# 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"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/isatest/annomaly.ML Tue Mar 20 20:42:14 2007 +0100
@@ -0,0 +1,26 @@
+use "ML-Systems/smlnj.ML";
+
+local
+
+ val smlnj_use_text = use_text
+
+ fun strip ([], name, _) = name
+ | strip (["Distribution"], name, _) = name
+ | strip (h1 :: t1, h2 :: t2, def) =
+ if h1 = h2 then strip (t1, t2, def) else def
+
+ fun rewrite (NONE, name) = "use_text" :: name
+ | rewrite (SOME home, name) =
+ strip (#arcs (OS.Path.fromString home), name, "use_text" :: name)
+
+in
+
+ fun use_text name p v t =
+ let val name = case name of "" => "unnamed" | name => name
+ val arcs = rewrite (OS.Process.getEnv "ISABELLE_HOME",
+ #arcs (OS.Path.fromString name))
+ val _ = AnnoMaLy.nameNextStream ("isabelle" :: arcs)
+ in smlnj_use_text name p v t
+ end
+
+end;
--- a/src/Pure/ML-Systems/annomaly.ML Tue Mar 20 17:07:23 2007 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,26 +0,0 @@
-use "ML-Systems/smlnj.ML";
-
-local
-
- val smlnj_use_text = use_text
-
- fun strip ([], name, _) = name
- | strip (["Distribution"], name, _) = name
- | strip (h1 :: t1, h2 :: t2, def) =
- if h1 = h2 then strip (t1, t2, def) else def
-
- fun rewrite (NONE, name) = "use_text" :: name
- | rewrite (SOME home, name) =
- strip (#arcs (OS.Path.fromString home), name, "use_text" :: name)
-
-in
-
- fun use_text name p v t =
- let val name = case name of "" => "unnamed" | name => name
- val arcs = rewrite (OS.Process.getEnv "ISABELLE_HOME",
- #arcs (OS.Path.fromString name))
- val _ = AnnoMaLy.nameNextStream ("isabelle" :: arcs)
- in smlnj_use_text name p v t
- end
-
-end;