Re: [isabelle-dev] AFP status
I already have Sturm_Tarski running again and will commit that later today. On a related note, in faf1aa9381e0, I also removed the definition of "algebraic" from Algebraic_Numbers and updated it to use the more general definition of "algebraic" that is now in the library. Cheers, Manuel On 13/01/16 08:56, Andreas Lochbihler wrote: Applicative_Lifting and Stern_Brocot now (AFP/1c0036f62a32) work with Isabelle/adcaaf6c9910. Andreas On 13/01/16 00:06, Makarius wrote: The AFP status is much better than last week, but these sessions are still broken (Isabelle/7355fd313cf8 and AFP/87337b54f3eb): Applicative_Lifting Stern_Brocot Sturm_Tarski In this hot phase of release preparation, we need things continuosly working. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle2016-RC0: potential changes
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?) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] next release
I don't expect to contribute anything else before the next release. There are little bits that I could add, but probably I should desist in the name of stability. Larry ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
