[isabelle-dev] Regain AFP sanity

Makarius makarius at sketis.net
Wed Jan 11 15:40:12 CET 2012

Dear all,

we've already got used to somewhat awkward AFP tests with many variants of 
failures and uninformative statistics like this random noise

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 ...

-------------- 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)

More information about the isabelle-dev mailing list