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 
  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 <>:
> 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-dev mailing list

Reply via email to