[isabelle-dev] Must the AFP be used as a component?

[Makarius]

On Sat, 15 Dec 2012, Florian Haftmann wrote:

> Hi all,
>
>> The reason is that Open_Induction/ROOT (and also
>> Open_Induction/Open_Induction.thy) relies on $AFP being set, which is
>> only the case if AFP is registered as a component (which is not the case
>> for Mira).
>
> I would recommend that mira incorporates AFP as component, since this is
> what we regularly recommend to users also.

I am not an administrator of AFP nor Mira, but my impression is that it is 
legitimate to have AFP not as component in some situations.  So within AFP 
the references to itself should be relative.

>
>> OT:  I just saw this: What is the reason for mira writing
>>
>>    init_components "$COMPONENT/contrib"
>> "$ISABELLE_HOME/Admin/components/main"
>>
>> instead of
>>
>>    init_components "$ISABELLE_HOME/contrib"
>> "$ISABELLE_HOME/Admin/components/main"
>>
>> to the settings file?

Note that isatest refers physically to the unpacked version of the 
component store like this:

   init_components /home/isabelle/contrib "$HOME/admin/components/main"

See also http://isabelle.in.tum.de/repos/isabelle/file/765c22baa1c9/Admin/isatest/settings/at-poly#l3

So there is no need to make another local copy.  Thanks to monotonicity 
and immutability of the component space, there should never be any 
concurrency issues.  Only the component maintainers ever write to the 
component file space.


Moreover see 
http://isabelle.in.tum.de/repos/isabelle/file/765c22baa1c9/Admin/components/README 
where I have tried to describe the situation for the 2-3 people who need 
to provide components, in order to reduce the administrative chaos a bit.


 	Makarius