# HG changeset patch
# User wenzelm
# Date 1364414830 -3600
# Node ID 5fffa75d24326e3e195c5d86785834ffa8a2ad65
# Parent  5b4ae246783038128c24651f22a5dbca82ca5033
separate isatest with skip_proofs, to give some impression of performance without most of the proofs;

diff -r 5b4ae2467830 -r 5fffa75d2432 Admin/isatest/isatest-makedist
--- a/Admin/isatest/isatest-makedist	Wed Mar 27 20:57:05 2013 +0100
+++ b/Admin/isatest/isatest-makedist	Wed Mar 27 21:07:10 2013 +0100
@@ -112,7 +112,8 @@
   $MAKEALL $HOME/settings/mac-poly64-M4;
   $MAKEALL $HOME/settings/mac-poly64-M8;
   $MAKEALL $HOME/settings/mac-poly-M4;
-  $MAKEALL $HOME/settings/mac-poly-M8"
+  $MAKEALL $HOME/settings/mac-poly-M8;
+  $MAKEALL $HOME/settings/mac-poly-M8-skip_proofs"
 sleep 15
 $SSH macbroy6 "$MAKEALL $HOME/settings/mac-poly64-M2"
 sleep 15
diff -r 5b4ae2467830 -r 5fffa75d2432 Admin/isatest/isatest-stats
--- a/Admin/isatest/isatest-stats	Wed Mar 27 20:57:05 2013 +0100
+++ b/Admin/isatest/isatest-stats	Wed Mar 27 21:07:10 2013 +0100
@@ -6,7 +6,7 @@
 
 THIS="$(cd "$(dirname "$0")"; pwd)"
 
-PLATFORMS="at-poly at-poly-test afp at64-poly mac-poly-M2 mac-poly-M4 mac-poly64-M2 mac-poly64-M4 mac-poly-M8 mac-poly64-M8 at-sml-dev"
+PLATFORMS="at-poly at-poly-test afp at64-poly mac-poly-M2 mac-poly-M4 mac-poly64-M2 mac-poly64-M4 mac-poly-M8 mac-poly-M8-skip_proofs mac-poly64-M8 at-sml-dev"
 
 ISABELLE_SESSIONS="
   HOL
diff -r 5b4ae2467830 -r 5fffa75d2432 Admin/isatest/settings/mac-poly-M8-skip_proofs
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/isatest/settings/mac-poly-M8-skip_proofs	Wed Mar 27 21:07:10 2013 +0100
@@ -0,0 +1,31 @@
+# -*- shell-script -*- :mode=shellscript:
+
+init_components /home/isabelle/contrib "$HOME/admin/components/main"
+
+  POLYML_HOME="/home/polyml/polyml-5.5.0"
+  ML_SYSTEM="polyml-5.5.0"
+  ML_PLATFORM="x86-darwin"
+  ML_HOME="$POLYML_HOME/$ML_PLATFORM"
+  ML_OPTIONS="-H 1000 --gcthreads 8"
+
+
+ISABELLE_HOME_USER=~/isabelle-mac-poly-M8-skip_proofs
+
+# Where to look for isabelle tools (multiple dirs separated by ':').
+ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
+
+# Location for temporary files (should be on a local file system).
+ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
+
+
+# Heap input locations. ML system identifier is included in lookup.
+ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
+
+# Heap output location. ML system identifier is appended automatically later on.
+ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
+ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
+
+ISABELLE_BUILD_OPTIONS="threads=8 skip_proofs"
+
+Z3_NON_COMMERCIAL="yes"
+
diff -r 5b4ae2467830 -r 5fffa75d2432 src/HOL/ROOT
--- a/src/HOL/ROOT	Wed Mar 27 20:57:05 2013 +0100
+++ b/src/HOL/ROOT	Wed Mar 27 21:07:10 2013 +0100
@@ -424,10 +424,6 @@
     "document/root.bib"
     "document/root.tex"
 
-session "HOL-MicroJava-skip_proofs" in MicroJava = HOL +
-  options [condition = ISABELLE_FULL_TEST, document = false, skip_proofs]
-  theories MicroJava
-
 session "HOL-NanoJava" in NanoJava = HOL +
   description {*
     Hoare Logic for a tiny fragment of Java.