Email Gateway (Aug 22 2022 at 09:27): Email Gateway (Aug 22 2022 at 09:27):From: Matthew Fernandez <matthew.fernandez@nicta.com.au>
Hi Isabelle folk,
As far as I'm aware, a session can only have a single parent:
session my_session = parent +
...
Sometimes I want to build on top of two previous sessions. The syntax makes it tempting to write:
session my_session = parent1 + parent2 +
...
However, this is invalid. So I typically achieve what I want with an intermediate base session:
session intermediate = parent1 +
... (* definition of parent2 repeated *)
session my_session = intermediate +
...
This works, but if theories in 'parent2' change, I end up effectively rebuilding its heap image
twice. Also, if someone changes the definition of 'parent2' and I fail to notice and update my
corresponding definition of 'intermediate' unexpected things may happen in future.
Is there a way to achieve this without an intermediate session? Failing that, is there a more robust
way to specify this intermediate session? It's possible I'm just not being creative enough in how
I'm choosing to define these sessions.
Thanks for your time,
Matthew
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Last updated: Apr 26 2024 at 12:28 UTC