Re: [isabelle] How to speed up locales

Hi Andreas,

if this refers to the development version of Isabelle -- this is a known problem. Certain performance improvements are currently disabled.

If you experience these problems with the last release, you probably have many lemmas with computational attributes like unfolded or simplified in you locales. These are show stoppers since they need to be executed whenever you enter a context.


Quoting Andreas Lochbihler <andreas.lochbihler at>:

Hi all,

I have a large system of locales with many sublocale declarations. My problem now is that opening some of the locales via "context ... begin" takes one minute or even longer (on a 2.33GHz processor with 4GB of memory). So I wonder how to adjust my theories such that this becomes faster.

Are there any rules of thumb how to organise a locale hierarchy to make it performant?
What are the do's and don'ts for efficient locales?

Thanks for any hints and ideas,

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