Re: [isabelle] THY path
thnx for the many answers!
@Tobias: between the AFP entries themselves I do exactly what you
However, the whole setup is more like Andreas described: n AFP entries
(currently 3, but I hope there are more to come) which we want to use in
our local development.
I do not particularly like the solution with adapting my local directory
structure. My current try is to have a local AFP.ML (see attachment)
adding the paths (to the local copy of the AFP hg-repo) and loading the
desired theories and then building a heap file
isabelle usedir -b -f AFP.ML HOL HOL-AFP
to work on. This almost works (and in our case the AFP entries are not
very big, hence creating the heap file is fast), only that there are
some THY files in AFP entries that have the same name as local THY
files... and this breaks everything. In the current situation it will be
easy to replace one file by a differently named one, but in general I
totally agree with Brian that the flat name space is... how to say...
not excessively nice.
On 09/17/2010 08:28 AM, Andreas Lochbihler wrote:
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
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.
well ^that sounds interesting... <whispering>how do I activate
NOTE: You have to set the environment variable ISAFOR_AFP
to the 'thys' directory of your local AFP copy, in order
for this file to work. This should be done in your
This archive was generated by a fusion of
Pipermail (Mailman edition) and