Email Gateway (Aug 18 2022 at 15:14): Email Gateway (Aug 18 2022 at 15:14):From: Andreas Lochbihler <andreas.lochbihler@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
Email Gateway (Aug 18 2022 at 15:14):From: Clemens Ballarin <ballarin@in.tum.de>
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@kit.edu>:
Email Gateway (Aug 18 2022 at 15:15):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Hi Clemens,
I am working with the official Isabelle2009-1 release, but there is not
a single [simplified] or [unfolded] attribute in my locales (other than
inside proofs). In this post in 2008,
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2008-May/msg00045.html
you suggested not to use computationally expensive attributes like
unfolded and simplified, so I have already hunted them down. What other
attributes should I hunt for?
The other thing is that my sublocale relationships are rather complex.
Here is a pattern that occurs multiple times in my theories:
-- Locale A fixes the parameters and B makes the assumptions:
locale A =
fixes f :: ...
and r :: ...
locale B =
A +
-- "Rename type variables back to what they were in A"
constrains f :: ...
and r :: ...
assumes ...
-- Locale C imports two copies of A and locale D adds the assumptions from B
locale C =
r1!: A f1 r1 +
r2!: A f2 r2
for f1 :: ...
and r1 :: ...
and f2 :: ...
and r2 :: ...
locale D =
C f1 r1 f2 r2 +
r1!: B f1 r1 +
r2!: B f2 r2
for f1 :: ...
and r1 :: ...
and f2 :: ...
and r2 :: ...
-- Apart from that, there is an orthogonal locale hierarchy E and F
locale E =
fixes g :: ...
and h :: ...
locale F =
E +
constrains g :: ...
and h :: ...
assumes ...
-- Now, some definitions (a and b) in locale E instantiate the
parameters of locale A and B:
definition (in E) a ...
definition (in E) b ...
sublocale E < s1!: A "a" "b x" for x .
sublocale F < s1!: B "a" "b x" for x ...
-- At some other place, other definitions (c and d) in E also
instantiate the parameters of A and B
definition (in E) c ...
definition (in E) d ...
sublocale E < s2!: A "c" "d y" for y .
sublocale F < s2!: A "c" "d y" for y .
Both of these instantiations are independent of each other in different
theories which then proceed to independent developments. However, there
is another thread of development where both are joined again:
-- Now, add C and D to E and F resp.
consts X :: ... -- "X is just a global constant"
sublocale E < t!: C "a" "b x" "c" "d (X x)" for x .
sublocale F < t!: D "a" "b x" "c" "d (X x)" for x ...
After this, opening the context E or F is especially slow, so I suspect
that this diamond pattern might be a bad design choice. Am I right? Are
there sublocale relationships that should be avoided? And are there
"design patterns" for good sublocale relationships?
Best,
Andreas
Email Gateway (Aug 18 2022 at 15:16):From: Clemens Ballarin <ballarin@in.tum.de>
Hi Andreas,
Instance is to be understood as a logical term. Two locale instances
are the same if they agree on the parameter instantiation. (Most of
the time, locales in fact use subsumption.) Prefixes are ignored.
There is no way of nitpicking locale content other than maintaining a
second locale manually.
Clemens
Quoting Andreas Lochbihler <andreas.lochbihler@kit.edu>:
Last updated: Apr 24 2024 at 04:17 UTC