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.

Clemens


Quoting Andreas Lochbihler <andreas.lochbihler at kit.edu>:

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,
Andreas








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