# HG changeset patch
# User gagern
# Date 1174419734 -3600
# Node ID 415098eece94e399e18bb3d2e4bf00f21ca67a39
# Parent  8cff8a6cb9956d4873800a15d1b2d21ff3b2e640
Changed AnnoMaLy build process from CVS to tarball sources.
Moved annomaly.ML from the official sources to the isatest directory.

diff -r 8cff8a6cb995 -r 415098eece94 Admin/isatest/annomaly
--- 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"
diff -r 8cff8a6cb995 -r 415098eece94 Admin/isatest/annomaly.ML
--- /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;
diff -r 8cff8a6cb995 -r 415098eece94 src/Pure/ML-Systems/annomaly.ML
--- 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;