--- a/Admin/isatest/isatest-makedist Wed Aug 01 15:46:45 2012 +0200
+++ b/Admin/isatest/isatest-makedist Wed Aug 01 15:50:50 2012 +0200
@@ -110,8 +110,8 @@
$SSH macbroy23 "$MAKEALL $HOME/settings/at-poly-e"
sleep 15
$SSH macbroy2 "
- env ISABELLE_BENCHMARK=true $MAKEALL $HOME/settings/mac-poly64-M4;
- env ISABELLE_BENCHMARK=true $MAKEALL $HOME/settings/mac-poly64-M8;
+ $MAKEALL $HOME/settings/mac-poly64-M4;
+ $MAKEALL $HOME/settings/mac-poly64-M8;
$MAKEALL $HOME/settings/mac-poly-M4;
$MAKEALL $HOME/settings/mac-poly-M8"
sleep 15
--- a/Admin/isatest/settings/mac-poly64-M4 Wed Aug 01 15:46:45 2012 +0200
+++ b/Admin/isatest/settings/mac-poly64-M4 Wed Aug 01 15:50:50 2012 +0200
@@ -26,4 +26,6 @@
ISABELLE_USEDIR_OPTIONS="-i false -d false -t true -M 4 -q 2"
ISABELLE_BUILD_OPTIONS="browser_info=false document=false threads=4 parallel_proofs=2"
+ISABELLE_FULL_TEST=true
+
init_component "$HOME/contrib_devel/kodkodi-1.2.16"
--- a/Admin/isatest/settings/mac-poly64-M8 Wed Aug 01 15:46:45 2012 +0200
+++ b/Admin/isatest/settings/mac-poly64-M8 Wed Aug 01 15:50:50 2012 +0200
@@ -26,5 +26,7 @@
ISABELLE_USEDIR_OPTIONS="-i false -d false -t true -M 8 -q 2"
ISABELLE_BUILD_OPTIONS="browser_info=false document=false threads=8 parallel_proofs=2"
+ISABELLE_FULL_TEST=true
+
init_component "$HOME/contrib_devel/kodkodi-1.2.16"
--- a/src/HOL/ROOT Wed Aug 01 15:46:45 2012 +0200
+++ b/src/HOL/ROOT Wed Aug 01 15:50:50 2012 +0200
@@ -740,7 +740,7 @@
Quickcheck_Narrowing_Examples
session Quickcheck_Benchmark = HOL +
- theories [condition = ISABELLE_BENCHMARK, quick_and_dirty]
+ theories [condition = ISABELLE_FULL_TEST, quick_and_dirty]
Find_Unused_Assms_Examples
Needham_Schroeder_No_Attacker_Example
Needham_Schroeder_Guided_Attacker_Example
@@ -874,7 +874,7 @@
session Datatype_Benchmark = HOL +
description {* Some rather large datatype examples (from John Harrison). *}
options [document = false]
- theories [condition = ISABELLE_BENCHMARK, timing]
+ theories [condition = ISABELLE_FULL_TEST, timing]
Brackin
Instructions
SML
@@ -883,6 +883,6 @@
session Record_Benchmark = HOL +
description {* Some benchmark on large record. *}
options [document = false]
- theories [condition = ISABELLE_BENCHMARK, timing]
+ theories [condition = ISABELLE_FULL_TEST, timing]
Record_Benchmark