Re: [isabelle] THY path



Hi,

thnx for the many answers!

@Tobias: between the AFP entries themselves I do exactly what you recommended.

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.

cheers

chris

On 09/17/2010 08:28 AM, Andreas Lochbihler wrote:
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.
well ^that sounds interesting... <whispering>how do I activate it?</whispering>

Andreas
(* 
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
  $ISABELLE_HOME_USER/etc/settings
file
*)
add_path "$ISAFOR_AFP/Abstract-Rewriting";
add_path "$ISAFOR_AFP/Matrix";
use_thys [
  "AbstractRewriting",
  "MatrixCarrier"
];


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