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

[Lars Noschinski]

On 17.12.2012 11:34, Makarius wrote:
> 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.

While this is the easiest setup, I think  we still allow use of isolated 
AFP entries, so not using it as a component is still a supported 
configuration.

As using the AFP as a component is unlikely to generate new problems, it 
is probably a good thing to test the configuration which is more likely 
to break.

>>> 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"

Actually, mira does this too, but with one more level of indirection:
/home/isabelle/contrib is symlinked to "$ISABELLE_HOME/contrib". Seems 
like a leftover from the pre-component days.

   -- Lars