Re: [isabelle] A single way to reference AFP entries



> So I wonder: Is it not possible to device a way that allows the same
> theories to work inside the AFP and outside? Why is it that within the
> AFP, $AFP cannot be set appropriately (to ".." if you want)?

Yes: you place the other AFP entries next to yours in the local directory structure, such that â../Entry/theoryâ refers to the correct theory.

This is indeed restrictive, because it determines your directory layout (some programming languages force that in any case), but once submitted to the AFP it is probably a good idea to at least keep it in its own isolated directory anyway, and having it organised such that AFP dependencies live next to it does make a certain sense.

I.e. something along the lines of

my-repo/
  other-things/
  AFP-things/
    my-entry/
    other-entry1/
    other-entry2/

Of course, AFP-things/ could be the root level or anywhere else in your structure, and there could be non-AFP things underneath it as well - this is just an example.


> The reason for .. mentioned above is that "it interacts correctly with
> multiple AFP installations side by side". But would setting AFP=.., if
> one has to work with multiple installations, not do the same?

Unfortunately not. $AFP is set as part of the component setup in the AFP itself - so whichever AFP installation you mention last in the component initialisation setup will be the one $AFP refers to.

Cheers,
Gerwin


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.


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