Email Gateway (May 03 2024 at 05:17): Email Gateway (May 03 2024 at 05:17):From: hannobecker@posteo.de
Hi Makarius and community,
There are a few outstanding reports of unexpected behaviour regarding
code generation, adhoc overloading, and locales.
Each report contains a minimal example to reproduce the behaviours, all
of which persist in Isabelle2024-RC3.
The reports are:
https://lists.cam.ac.uk/sympa/arc/cl-isabelle-users/2024-02/msg00053.html
(Failure of lift_definition in the context of type classes.)
https://lists.cam.ac.uk/sympa/arc/cl-isabelle-users/2024-01/msg00079.html
(Constant folding during code generation from locales and sublocales)
https://lists.cam.ac.uk/sympa/arc/cl-isabelle-users/2024-02/msg00015.html
(Adhoc Overloading corrupted by unrelated definition)
These behaviours arise in a large-scale application of Isabelle making
extensive use of nested locales, code generation, and adhoc overloading.
We are currently carrying ad-hoc (no pun intended) patches to
adhoc_overloading because of the last report.
I appreciate that investigating these reports is time-consuming and, by
now, not an option for Isabelle2024 anymore. Moving forward, however,
thoughts would be appreciated on how to explain/address them. If there
is a place where such open reports are gathered, that would also be
helpful to know, so they cannot be forgotten.
Thanks for the hard work,
Regards,
Hanno
Email Gateway (May 03 2024 at 09:19):From: Kevin Kappelmann <kevin.kappelmann@tum.de>
Attached you can find a patch for the third report. I leave it up to
Makarius whether this can still be included in Isabelle2024.
The issue is that variants_eq in adhoc_overloading.ML checks
equality of types syntactically, but it has to check it up to renaming
of schematics.
(In the example of the report, the types ?'a -> ?'a and ?'a1 -> ?'a1
weren't identified)
Best wishes,
Kevin
type_eq_adhocoverloading.patch
Last updated: May 19 2024 at 04:18 UTC