Re: [isabelle] A single way to reference AFP entries


Am Freitag, den 20.05.2016, 13:52 +0200 schrieb Lars Hupel:
> > 
> > So I wonder: Is it not possible to device a way that allows the same
> > theories to work inside the AFP and outside? Why is it that within the
> > AFP, $AFP cannot be set appropriately (to ".." if you want)?
> There are mostly technical reasons for this, affecting both users and
> the testing infrastructure. Gerwin has already explained the former.
> The effect on the testing infrastructure is that building the AFP would
> require component setup, which is problematic when paths are not known.
> Isabelle would need to be aware of concrete paths of things on the build
> servers (which are not constant).

ok, let me phrase the question differently:
What could and should changed, either in Isabelle or the AFP component
setup, so that it _becomes_ possible to use the theories in both setups
(within the AFP directory structure, as well as stand-alone theories
using the registered AFP component)?


Dr. rer. nat. Joachim Breitner
Wissenschaftlicher Mitarbeiter

Attachment: signature.asc
Description: This is a digitally signed message part

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.