[isabelle-dev] Isabelle2016-RC0: potential changes

Makarius makarius at sketis.net
Wed Jan 13 21:26:21 CET 2016

On Mon, 11 Jan 2016, Manuel Eberl wrote:

> I also noticed the ring_gcd instance for polynomials. Finalising the 
> changes to the GCD class hierarchy and updating the AFP entries that 
> rely on half-finished versions of this change (such as Echelon_Form) is 
> something that I should probably take care of soon, but definitely not 
> before the 2016 release – hopefully before the 2017 one.

Note that 2016 is what could be called an "Isabelle leap-year".  With a 
release near the start, there needs to be a second one near the end. The 
distance between releases is constant at approx. 8-10 months.

At some point we've tried to target exactly 12 months, but that resulted 
in 25 months, and a commitment to the strict 8-10 months rule afterwards.

Interestingly, the Coq guys are trying for years to target 12 months as 
well, but the 8.5 release is already much longer in the pipeline. (More 
than 3 years?)


More information about the isabelle-dev mailing list