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