Re: [isabelle] Session with multiple parents



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




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