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
> 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:
date: Wed Jan 11 21:30:05 2012 +0100
method "cond_eval" reduces total runtime to a few minutes if
user: Lars Hupel <lars.hupel at mytum.de>
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