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

[Tobias Nipkow]

Am 17/12/2012 11:34, schrieb 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.

Makarius is right, the AFP pages tell you how to install the AFP as a component,
but that is merely a convenient option.

Tobias

>>
>>> 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
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev