# Re: [isabelle-dev] Towards the Isabelle2017 release

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.
>
>
>
> 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