Dear all, let me share my opinions after porting IsaFoR to yesterdays development version:
- In total the transition from our 2016-1 source went quite smooth (~ 14 hours for whole of IsaFoR) - Most changes have been caused by integrating session-qualified theory imports. This will also require a reform of the splitting of sessions, which previously was structured towards a fast build-process, but now should be structured more towards logical structure (which is currently reflected in the directory-structure). - In the NEWS I read about freeing short constant names like the “Renamed ii to imaginary_unit in order to free up ii as a variable”. I definitely support this kind of change, but at the same time found quite the opposite in HOL-Algebra: If one imports HOL-Algebra.Multiplicative_Group (which we actually do via some transitive import), then \mu (LFP), \nu (GFP) and \phi (Euler’s totient function) become constants. This was a bit annoying. - There have been some changes w.r.t. code-generation which now lead to runtime exception in the generated code. For instance, now I get code like “f x = Code.abort …” whereas in 2016-1 there was a proper code like “f x = some ordinary right-hand side” We did not yet isolate the problem and will report later. Cheers, René > Am 21.08.2017 um 20:24 schrieb Makarius <makar...@sketis.net>: > > Dear Isabelle contributors, > > we are now definitely heading towards the Isabelle2017 release. > > The first official release candidate Isabelle2017-RC1 is anticipated for > 2/3-Sep-2017, that is a bit less than 2 weeks from now. > > That is also the deadline for any significant additions. > > > I have already updated the important files NEWS, CONTRIBUTORS, ANNOUNCE > in Isabelle/5c0a3f63057d, but it seems that many potential entries are > still missing. > > Please provide entries in NEWS and CONTRIBUTORS for all relevant things > you have done since the last release. > > > 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