[isabelle-dev] Regain AFP sanity

[Makarius]

Dear all,

we've already got used to somewhat awkward AFP tests with many variants of 
failures and uninformative statistics like this random noise
http://isabelle.in.tum.de/devel/stats/afp.html


The problem seems to boil down to the two really big sessions, because 
they prevent frequent painless testing:

   Flyspeck-Tame (approx. 6-9h runtime)
   JinjaThreads (approx. 1-2h runtime, up to 32 GB memory)

Big applications are not a problem as such, but we should make an effort 
to regain some sanity in everyday testing.  If isatest is moved back to a 
predicable machine like macbroy2 we could get back to useful statistics 
for big applications as well.


To make a start, the included changeset for Flyspeck-Tame reduces the 
total runtime to a few minutes, while still doing some meaningful tests. 
To refine this, one could easily make a private version of the "eval" 
method in theory ArchComp that depends on an external environment variable 
like "AFP_FULL_TEST" to control this.  That setting would then be off by 
default, but enabled in certain isatest/mira runs.

For JinjaThreads we will have to spend much further thoughts, though ...


 	Makarius
-------------- next part --------------
# HG changeset patch
# User wenzelm
# Date 1326291977 -3600
# Node ID 5186b20b994ca8115f6018b2d0ab5cee79a8bca9
# Parent  3ee574b55d0917ddcef070ff220ca8e8ec51dc9b
skip some really long proofs;

diff -r 3ee574b55d09 -r 5186b20b994c thys/Flyspeck-Tame/ArchComp.thy
--- a/thys/Flyspeck-Tame/ArchComp.thy	Wed Jan 11 09:23:11 2012 +0100
+++ b/thys/Flyspeck-Tame/ArchComp.thy	Wed Jan 11 15:26:17 2012 +0100
@@ -8,6 +8,8 @@
 
 subsection {* Proofs by evaluation using generated code *}
 
+axioms eval: A
+
 lemma pre_iso_test3: "\<forall>g \<in> set Tri. pre_iso_test g"
 by eval
 
@@ -24,12 +26,12 @@
 by eval
 
 lemma same4: "samet (tameEnumFilter 1) Quad"
-by eval
+by (rule eval)
 
 lemma same5: "samet (tameEnumFilter 2) Pent"
-by eval
+by (rule eval)
 
 lemma same6: "samet (tameEnumFilter 3) Hex"
-by eval
+by (rule eval)
 
 end