Re: [isabelle] [ExternalEmail] [isabelle-dev] afp-2016-1 branch

On 06/12/16 09:32, Lars Hupel wrote:
>> As for other AFP entries, like Flyspeck_Tame, we have a few ones that
>> are too big to test on every push like the rest of the AFP and those get
>> tested in isabelle-nightly-slow. I don't know the AFP in enough detail
>> to say with certainty that none of them contains any parts that are
>> skipped during these tests like Flyspeck_Tame used to, but I don't think
>> so, given that that testing such things is the express purpose of
>> nightly-slow.
> I did check for build conditions and occurrences of ISABELLE_FULL_TEST.
> All of these should have been eliminated. In case anyone notices
> leftover conditional builds (except for code generator checks), that
> would be a bug.

The word "bug" always triggers critical questions. Can you explain the
point of removing the conditional build?

We are talking about these two changesets:

changeset:   2646:3dcc6b9eae2b
user:        wenzelm
date:        Wed Jan 11 21:30:05 2012 +0100
files:       thys/Flyspeck-Tame/ArchComp.thy
method "cond_eval" reduces total runtime to a few minutes if

changeset:   6524:cac201d3f3f9
user:        Lars Hupel <lars.hupel at>
date:        Fri Apr 15 17:28:43 2016 +0200
files:       thys/Flyspeck-Tame/ArchComp.thy thys/Flyspeck-Tame/ROOT
full test for Flyspeck-Tame; get rid of ISABELLE_FULL_TEST

The optional version of Flyspeck-Tame had the advantage that the
relevant part for the test always happens quickly (without "slow" or
"very_slow" categorization). The full test -- which never failed in its
whole history -- was done once and a while (I think weekly).

This saved both CPU time and interactive testing time: I now find myself
doing manual Flyspeck-Tests, imitating the missing condition in the
Prover IDE by hand.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.