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



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 Mon, Dec 5, 2016 at 11:28 PM, 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
>>
>>
>>




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