[isabelle-dev] AFP as Isabelle component

[Makarius]

On Thu, 25 Aug 2011, 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

The idea behind components is to make things modular, movable, pluggable. 
This means one should avoid hardwired locations such as ~~/contrib/afp/.

The usual way is to invent a suitable name for environment settings, such 
as AFP_HOME at have the component provide that; possibly with AFP_THEORIES 
as something like "$AFP_HOME/thys" or whatever.  See also existing example 
components from the Isabelle distribution "bundle".

Users can then refer "$AFP_HOME/.../My_Theory" in regular theory imports.


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

There has been indeed a bit of divergence of the traditional isabelle 
make/build script setup and the one of AFP, which is a bit younger.  None 
of these are worth keeping indefinitely, though, and I would like to see a 
new unified build system as part of the Isabelle/Scala layer soon.  (Then 
we will also disvover further accidents like the duplicate HOL-Matrix 
sessions in Isabelle/HOL vs. AFP.)


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

AFP seems to be lagging behind concerning naming sessions, sticking to the 
historical accident of "-" to separate words, instead of "_". This will 
become practically relevant when session names become name space prefixes, 
because List-Infinite.List2.ilist is not an identifier within the formal 
language.


 	Makarius