[isabelle-dev] AFP as Isabelle component

Gerwin Klein gerwin.klein at nicta.com.au
Fri Aug 26 01:21:14 CEST 2011

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


Version: GnuPG/MacGPG2 v2.0.16 (Darwin)


More information about the isabelle-dev mailing list