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



On 23/12/16 05:25, Thomas.Sewell at data61.csiro.au wrote:
> 
> 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.
> 
> 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.

This sounds like requiring 5-10 more manpower behind Isabelle
development and release process.

Even just having "patch levels" with small amendments for published
releases (as done for Coq), already requires significant extra time.

Isabelle releases do not even have version numbers: every release is a
consolidated state of ongoing linear development. In the past, the
consolidation required 2-3 weeks, but we are now approaching 6-8 weeks
(with relatively little happening in that long time).


	Makarius






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