Re: [isabelle] Performance regression in 2016-1 with character strings.



> On 17.12.2016, at 01:26, Makarius <makarius at sketis.net> wrote:
> 
> On 16/12/16 14:55, Makarius wrote:
>> On 16/12/16 05:54, Thomas.Sewell at data61.csiro.au wrote:
>>> 
>>> We're sorry we didn't notice how significant the impact was until after 
>>> the release.
>> 
>> Can you explain what went wrong in the release process?
>> 
>> The first release candidate on 01-Nov-2016, more than 6 weeks ago.
> 
> Sorry, I've got this wrong.
> http://sketis.net/2016/release-candidates-for-isabelle2016-1 says:
> 
>  On 28-Oct-2016 the release candidate Isabelle2016-1-RC1 was published.
> Serious testing by users is now required, to expose remaining problems.
> 
> 
> That was exactly 7 weeks ago -- a very long time. Since such
> post-release problems of users have happened routinely in recent years,
> I would like to know what can be done about it.

I donât think there is much that can be done from the release side. 7 weeks is a good period for testing for ânormalâ users, but it is not a lot of time to update > 500kloc of proof from one Isabelle release to another when there are too many other pressing things to do. We did manage to test functionality in time, but not performance, and that was mostly a function of what testing hardware we had available on our end (a particular bottleneck this year).


> Maybe we should offer some "premium user" program: Improvements of
> published releases are charged $$$.

Might be an idea, but currently not necessary, at least not for us :-) Itâs relatively easy to change things on our side, it would just have been nicer for the rest of the community if we had managed to find the problem earlier. Maybe nobody else needs that many string comparisons â the performance regression didnât seem to show up in a major way in the AFP or distribution after all.

Cheers,
Gerwin


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