Email Gateway (Dec 14 2020 at 20:37): Email Gateway (Dec 14 2020 at 20:37):From: Clemens Ballarin <ballarin@in.tum.de>
Locales do not have many means for debugging a development. But even the
tools that are available seem not as widely known as I thought. I would
like to highlight two:
Method 'intro_locales'. Unlike its sibling 'unfold_locales' it does
not descend into locale assumptions but leaves statements involving
locale predicates in the goal state. This makes immediately clear which
locale instances the goals originate from. While 'unfold_locales' is
part of the default method of 'proof' and often invoked behind the
scenes, 'intro_locales' needs to be invoked manually.
Attribute 'trace_locales'. This is a recent addition (Isabelle 2020).
When set to 'true', prints the locale instances activated during
roundup. This can be helpful when locale commands yield obscure errors
due to conflicting syntax or for understanding local theories created by
complex locale hierarchies.
I have amended the Isar Reference Manual (development version)
accordingly, so these hints will become part of the documentation.
Clemens
Email Gateway (Jan 10 2021 at 18:27):From: Makarius <makarius@sketis.net>
Something to read and try in the current release candidate:
https://isabelle.in.tum.de/website-Isabelle2021-RC2
Makarius
Last updated: Apr 25 2024 at 20:15 UTC