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



Sorry I haven't been around for this discussion.

Thanks Florian for the patch. We've also found a similar fix, we'll 
adopt one or
the other locally until the next release.

About Makarius' question:

Since such
post-release problems of users have happened routinely in recent years,
I would like to know what can be done about it.


It's worth thinking about this. Ideally we'd see releases go out with no 
problems
remaining in them.

However, the only strategy that has been considered yet is to wait long 
enough
during the pre-release phase for all "serious users" to update their 
proofs. I don't
think we're going to be able to do that. On this occasion, we had a 
volunteer, and the
INCOMPATIBILITY level wasn't so bad (the changes to supremum sets being 
the worst
offenders), and still, we finished the update process shortly after the 
release became
official. This was a good release. In previous releases we've been 
preoccupied with
other things, and have stayed on the previous Isabelle version for months.

Another possible strategy would be to split Isabelle releases between 
compatible
releases (new features, PIDE extensions etc) and incompatible releases
(INCOMPATIBILITY allowed). "Serious users" could then do push-button 
tests and
offer feedback on all compatible releases. This is known to be a reasonable
strategy, since it's what pretty much every mature system out there does,
but it's probably too much to hope that Isabelle development would change
so substantially.

We can also suggest particular test cases that match the kinds of 
problems we
have locally. For instance, it's obvious that we could stress-test 
string comparisons
with a fairly short theory, and contribute that as a test case. Likewise 
our problems
with large records. But it's a lot of work to discover an essential test 
case.
For this release, it took three of us most of a day to
narrow down the performance problems we were seeing from polymorphic 
constants
on C-types to the simple issue of string comparison.

Anyway, if anyone else has any bright ideas how we can help, we'd be 
happy to.

Cheers,
    Thomas.

On 17/12/16 16:02, Klein, Gerwin (Data61, Kensington NSW) wrote:
>> 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.