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
towards logical structure (which is currently reflected in the
- 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.
> 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.
> isabelle-dev mailing list
isabelle-dev mailing list