Re: [isabelle] THY path



Hi Chris,

> The reason is that we have 3 entries in the AFP which our development is based on (currently we have local copies of the corresponding THY files). To me, it would seem as an overkill, if I had to incrementally construct heap images for
> 1) HOL-First-Entry
> 2) HOL-First-and-Second-Entry
> 3) HOL-First-and-Second-and-Third-Entry
> and then use 'HOL-First-and-Second-and-Third-Entry instead' of 'HOL'.
> 
> What do you think? How do other users that base their work on AFP entries, handle such situations? Andreas? ;)
JinjaThreads, which I am working on, also builds on three other AFP entries (Coinductive, FinFun and Jinja/DFA) and HOL-Word. The JinjaThreads theories in the AFP use the import system with relative paths explained by Tobias and use the HOL-Word heap.
Gerwin suggested to me that I do not build incremental heaps (HOL, HOL-Word, HOL-Word-Coinductive, HOL-Word-Coinductive-FinFun, ...), but rather pick one of them (HOL-Word) as the basis and load the other's theories on demand. This way, while building JinjaThreads, Isabelle loads also the other AFP entries again.

For my everyday development on JinjaThreads I have given up on building images of the other AFP entries and working with them because I update my Isabelle version to the latest repository snapshot every two or three days. So, I would have to rebuild these heap images each time then. Instead, I have organised my local directory structure to match the AFP's. To get to work quickly, I simply load these base theories with the "skip proof" option enabled, which is fairly fast.

Andreas







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