[isabelle-dev] Towards the Isabelle2017 release

[Thiemann, Rene]

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 <makarius at 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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev