[isabelle-dev] Must the AFP be used as a component?
noschinl at in.tum.de
Mon Dec 17 11:57:18 CET 2012
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
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
>>> OT: I just saw this: What is the reason for mira writing
>>> init_components "$COMPONENT/contrib"
>>> instead of
>>> init_components "$ISABELLE_HOME/contrib"
>>> 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.
More information about the isabelle-dev