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

[Gerwin.Klein at data61.csiro.au]

Hi Randy,

there are a few sessions with the tag “slow” in the AFP, of which Flyspeck_Tame is one. These are tested once a day. All other sessions are tested with each push.

Cheers,
Gerwin 


> On 6 Dec 2016, at 12:28 AM, Randy Pollack <rpollack0 at gmail.com> wrote:
> 
> Gerwin,
> 
> I was looking at the Flyspeck_Tame entry in the AFP today.  The
> current version of proofs built in Isabelle 2016 in a few minutes.
> But there is more to this development than checking the proofs.  There
> are "Proofs by evaluation using generated code" that are only executed
> if ISABELLE_FULL_TEST=true.  These proofs by evaluation take several
> hours to run.
> 
> I wonder if these proofs by evaluation are checked when the AFP is
> brought up-to-date with a new release of Isabelle?  Similarly, do
> other AFP entries have parts that may not be getting checked with new
> releases.
> 
> Thanks for any info.
> 
> --Randy
> 
> On Wed, Nov 30, 2016 at 11:46 AM,  <Gerwin.Klein at data61.csiro.au> wrote:
>> As of 61df7b06f131 there is now a new branch afp-2016-1, which will become the new afp release branch when Isabelle2016-1 is released.
>> 
>> Any further changes to afp-devel will now by default not show up in this branch.
>> 
>> Cheers,
>> Gerwin
>> 
>>> On 28 Nov 2016, at 6:08 PM, gerwin.klein at data61.csiro.au wrote:
>>> 
>>> Since the Isabelle2016-1 release is approaching, we will be preparing the new afp-2016-1 release branch as well.
>>> 
>>> If there are any urgent changes or updates to afp-devel that still need to go into afp-2016-1, please let me know. I am planning to fork off the branch in two days. Changes after that will not make it into the release.
>>> 
>>> Cheers,
>>> Gerwin
>>> 
>>> _______________________________________________
>>> isabelle-dev mailing list
>>> isabelle-dev at in.tum.de
>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>> 
>> 
>>