[isabelle-dev] AFP as Isabelle component

[Gerwin Klein]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1


On 26/08/2011, at 7:23 AM, Florian Haftmann wrote:
> I remember that once there was a discussion how AFP theories could be
> referenced in theory headers using an environment variable AFP_THEORIES
> or something similar.
> 
> Maybe the afp could be turned into an optional Isabelle component, e.g.
> at ~~/contrib/afp.  This would be have a couple of technical advantages:
> a) Canonical path for importing AFP theories, e.g ~~/contrib/afp/thys

Sounds good to me.


> b) Turning AFP testall into an Isabelle tool, eliminating the need for
> the -t option and similar things

Not sure I would like that, but it's an orthogonal problem.


> c) A clear association of Isabelle distribution of AFP, with facilitates
> having different Isabelle repositories on the same machine

Apart from the fact that the AFP is getting really large and you probably don't want a lot of many copies of it on your machine. But the possibility for those that do would be there.


> d) Standardized directory structure, which is important for the ever
> more critical matter of integration.

Not sure what you mean, but it sounds positive ;-)

There are a few (solvable, I think) problems with this: 
- - The idea for users of the AFP is that they can download a single entry or a set of entries. We should not require or expect the whole AFP to be there. No reason it has to be the whole AFP in ~/contrib, though
- - You don't want an hg repository inside an hg repository
- - AFP users should only see things under afp/thys/, i.e. the path for an AFP entry should be ~~/contrib/afp/Entry

Cheers,
Gerwin

-----BEGIN PGP SIGNATURE-----
Version: GnuPG/MacGPG2 v2.0.16 (Darwin)

iQCVAwUBTlbY8x4jbukySXM5AQIiLAQAjxQd1YFdn6yS/aabYl9sqooCxl2xoKOk
L2YPDemZee9IK7OyDcTCEvZEYf2L5o1vT8gxIWzNXV9BinVeTdpIBZ1jVFZQkxeR
4bkSJzNr15oBXxhDtItIzIcX/Bj7xiPGg2W62rEBOEmfN5ILQvvr+QaQJBxIGNUT
qtVl/dW/SG0=
=vUHO
-----END PGP SIGNATURE-----