[isabelle-dev] AFP as Isabelle component
gerwin.klein at nicta.com.au
Fri Aug 26 01:21:14 CEST 2011
-----BEGIN PGP SIGNED MESSAGE-----
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
-----BEGIN PGP SIGNATURE-----
Version: GnuPG/MacGPG2 v2.0.16 (Darwin)
-----END PGP SIGNATURE-----
More information about the isabelle-dev