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



I don't know whether or not this was done in the past, but Lars Hupel
removed this conditional evaluation from Flyspeck_Tame in April 2016 [1]
when he introduced the new CI infrastructure.

All of Flyspeck_Tame now gets tested once a day (it is part of the
isabelle-nightly-slow job in Isabelle/Jenkins [2]).

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.

Cheers,

Manuel


[1]
https://bitbucket.org/isa-afp/afp-devel/diff/thys/Flyspeck-Tame/ArchComp.thy?diff1=65cbeb22452d5e6f526758d8ff98bb942f1f0077&diff2=cac201d3f3f9&at=default

[2] https://ci.isabelle.systems/jenkins/job/isabelle-nightly-slow/




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