Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle2020-RC1: migration and performance

Email Gateway (Aug 23 2022 at 08:45):

From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear Makarius,

thanks for taking care of the release of Isabelle 2020.

From the IsaFoR side I can report that

• the migration to Isabelle 2020 was quick and easy (one afternoon) taking the following steps:

  • adjusted ROOT file
  • rewrite usages of UNION and INTER

  • eliminate name conflicts, mostly via "hide_const (open) FuncSet.Pi” and similar statements
    (somehow the FuncSet theory gets imported much earlier than before)

  • nothing else was required

• the processing time slightly went up:

  & HOL-Lib & HOL-AFP & IsaFoR\_1 & IsaFoR\_2 & IsaFoR\_3 & IsaFoR\_4 & Code
  theories & 195 & 421 & 138 & 64 & 151 & 21 & 1
  Isabelle 2019 & 4:55 & 7:14 & 5:25 & 5:37 & 7:38 & 8:33 & 7:12
  Isabelle 2020-RC1 & 5:44 & 9:28 & 6:12 & 6:03 & 8:58 & 9:58 & 7:34

Best regards,
René
signature.asc

Last updated: Apr 19 2024 at 20:15 UTC