Re: [isabelle] THY path

On Thu, Sep 16, 2010 at 5:45 AM, Christian Sternagel
<christian.sternagel at> wrote:
> Hi!
> is there a way of telling Isabelle where to search for THY files? From the
> error message in PG-Emacs when trying to load a non-existing THY file, I get
> that the standard search is "." and "$ISABELLE_HOME/src/HOL/Library". I
> would like to extend this list.

In src/HOL/Plain.thy, you'll find the following line:

ML {* path_add "~~/src/HOL/Library" *}

You can add similar lines to your own theory files if you want to add
other directories to the search path. This one uses "~~" and so is
relative to $ISABELLE, but I think absolute paths should also work.

> 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'.

It is a real shame that building custom heap images is so difficult. I
agree that having to build N heap images in sequence just to use N
different libraries at once is overkill. A nicer solution would be to
have a tool where you could say "give me a heap image with libraries
X, Y, and Z" and it would compile one for you in one step.
Unfortunately, the current Isabelle tools are based on an assumption
of one-heap-image-per-directory; we really need to move away from

> What do you think? How do other users that base their work on AFP entries,
> handle such situations? Andreas? ;)
> cheers
> chris

Question from Isabelle newbie: "This AFP library looks interesting;
how do I install it?" My shameful response is that by far the easiest
way to use an AFP library is to copy all the files into a directory
with all your own theory files. I know that this doesn't scale well if
you want to use more than one AFP library at once. You could use
separate directories and relative paths as Tobias suggests, but as
long as we have a flat theory namespace this doesn't really scale
either. (Question for the AFP maintainers: With about 80 AFP entries
now, do they all use distinct theory names? Is this something that you
should be worried about?)

Being able to download and use other people's Isabelle libraries (AFP
entries in particular) is very important, in my opinion, and the
current situation is unacceptable. I think that having a proper way to
"install" third-party Isabelle libraries would bring significant
benefits to our research community, making it much easier for people
to collaborate and build upon each other's work.

I really hope that most of the developers will continue to think about
how we can do this better.

Thanks, Chris, for bringing this issue to everyone's attention.

- Brian

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