Email Gateway (Aug 19 2022 at 11:22): Email Gateway (Aug 19 2022 at 11:22):From: Matthew Fernandez <matthew.fernandez@nicta.com.au>
Hi all,
Apologies if this question has already been answered, but I could not
find a nice solution.
Section 3.1 of the Isabelle system manual describes the format
describing a session. The discussion in this section and surrounding
implies that the session hierarchy is a tree and perhaps sessions cannot
have multiple parents. I can construct this relationship by having a
session A with parent B, that also imports a theory from session C. Is
there a nicer way of doing this? Basically I want to write:
session A = B + C + body...
but it seems this is not permissible. Any advice would be greatly
appreciated.
Thanks,
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.
Email Gateway (Aug 19 2022 at 11:43):From: Makarius <makarius@sketis.net>
On Thu, 25 Jul 2013, Matthew Fernandez wrote:
Section 3.1 of the Isabelle system manual describes the format
describing a session. The discussion in this section and surrounding
implies that the session hierarchy is a tree and perhaps sessions cannot
have multiple parents.
Yes, the overall hierarchy of sessions is a tree. The word is mentioned
explicitly on page 19 of the manual, where the form
session A = B + body
is explained. I see 2 or 3 more occurrences of "tree" in the manual.
I can construct this relationship by having a session A with parent B,
that also imports a theory from session C. Is there a nicer way of doing
this? Basically I want to write:session A = B + C + body...
but it seems this is not permissible. Any advice would be greatly
appreciated.
Sessions cannot be merged. Normally you just figure out one main line in
the tree path, and import further theories side-ways by loading the theory
sources again. (A system of "separate compilation" as available in Coq
would allow such fine-grained merges of precompiled modules, but it has
other performance problems.)
Conceptually, session images are of relatively little importance. They
are mainly a physical snapshot of a certain situation. Build and load
times of big applications may be fine-tuned by smart arrangement of
session images -- sometimes it just means to avoid redundant intermediate
images, because these are also synchronization points for parallel proof
processing: one process needs to finish before another can be started.
Just loading everything you need in one big session, e.g. starting from
HOL, might be not as bad as expected. Historically it was not done by
default due to various technical snags that no longer exist. E.g. I can
load all of AFP/JinjaThreads comfortably into one big session on my cheap
laptop, starting from HOL-Word, for example.
For AFP as big library the situation is slightly different: certain
session images that are re-used a lot help to speed up the overall build
process. (The isabelle build tool could be smarter to make such
arrangements automatically.)
Makarius
Last updated: Apr 30 2024 at 04:19 UTC