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



> 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).




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