Email Gateway (Aug 22 2022 at 20:29): Email Gateway (Aug 22 2022 at 20:29):From: Clemens Ballarin <ballarin@in.tum.de>
There is now a new configuration attribute "trace_locales". When set,
via
declare [[trace_locales]]
locale instances activated during roundup are printed. I find this more
useful than the existing diagnostic commands:
print_dependencies <expression>
print_interps <locale>
I consider removing these latter commands altogether, and I would
therefore like to know whether they are used.
Clemens
Email Gateway (Aug 22 2022 at 20:29):From: Makarius <makarius@sketis.net>
BTW, isabelle-users is for official releases. The above refers to
ongoing repository development at revision d997c7ba3305.
The next release is presumably Isabelle2020 (June 2020), release
candidates starting 8 weeks before that.
Makarius
Email Gateway (Aug 22 2022 at 20:38):From: Clemens Ballarin <ballarin@in.tum.de>
Dear Isabelle Users,
I haven't received any feedback on whether the current diagnostic
commands 'print_dependencies' and 'print_interps' are used. Also, there
is only a single invocation in the entire Isabelle distribution and AFP.
So it looks like these commands can indeed be removed for Isabelle
2020. As announced, the intended replacement is already available for
evaluation in the Isabelle development snapshot.
Clemens
Email Gateway (Aug 22 2022 at 20:38):From: "Klein, Gerwin (Data61, Kensington NSW)" <Gerwin.Klein@data61.csiro.au>
I’m happy with removing these, but I’d like to point out that them not occurring in the AFP or the Isabelle distribution is not an indication for not-use. They are diagnostic commands and shouldn’t be there even if they were used every day.
Cheers,
Gerwin
Last updated: Apr 26 2024 at 20:16 UTC