[isabelle-dev] Must the AFP be used as a component?
makarius at sketis.net
Mon Dec 17 11:34:05 CET 2012
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"
>> 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"
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.
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.
More information about the isabelle-dev