[isabelle] A short report on updating IsaFoR to Isabelle 2018 RC0



Dear all,

here is a short report on my experience after updating all of IsaFoR from 
Isabelle 2017 to Isabelle 2018 RC0.

- In total, the transition went quite smooth by using the information
  that was provided in the NEWS file. 
  It took only 12 hours to update the 213k lines of theory files,
  including IsaFoR-compilation times. 

- The tools “isabelle update_op”, Rafal Kolanski’s “goto_error” macro, and
  the indication of error-free theories via bold-boxes in the Theories-panel 
  were all very helpful.

- The most tedious update task was changing all the occurrences of “def” 
  into “define”. In particular, the duplication of the name was annoying,
  e.g., changing < def \<sigma> == some_exp > into < define \<sigma> where "\<sigma> == some_exp” >.
  If possible, it would be nice to have a short form available in Isabelle 2018 like
  it is possible with “definition”: < define "\<sigma> = some_exp” > would be nice.

- I would have expected a statement in the NEWS file 
  on the necessary import of "HOL-Library.Lattice_Syntax”.

- The most difficult update was the change of the “rewrites” and “defines” 
  conditions in locale interpretations where it now does not seem possible
  anymore, to define “rewrite"-rules that depend on newly defined constants
  from the “defines” part. 
  (I wrote a separate e-mail to Clemens B. on this issue)

- The most visible impact from our side is the deletion of Code_Char.
  The result is that our generated code became
  - 3x larger: from 2575550 bytes to 7848600 bytes
  - much less readable: compare the previous string 
         “ is symbol …” 
    in the generated code which now became
         [Char False False False False False True False False,
          Char True False False True False True True False,
          Char True True False False True True True False,
          Char False False False False False True False False,
          Char True True False False True True True False, …]
    where every character is expanded into a whole line
  - 1.5x slower on average, when running on it on an 2359 examples (30 min before, now 45 min)
  
Cheers,
René



> Am 06.06.2018 um 17:08 schrieb Makarius <makarius at sketis.net>:
> 
> Dear Isabelle users,
> 
> the Isabelle2018 release is scheduled for August 2018, approx. 10 weeks
> from now. The first official release candidate can be anticipated in 4
> weeks.
> 
> In order to get started with proper testing, there is now an informal
> snapshot Isabelle2018-RC0 (see
> https://isabelle.in.tum.de/website-Isabelle2018-RC0).
> 
> The ongoing release process is continuously documented at
> see also https://sketis.net/2018/release-candidates-for-isabelle2018
> 
> 
> When discussing observations about release candidates, please provide
> a Subject: line that fits to the content, not just a clone of the
> announcement.
> 
> 
> 	Makarius
> 



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.