[isabelle-dev] AFP as Isabelle component
makarius at sketis.net
Fri Aug 26 13:03:45 CEST 2011
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
More information about the isabelle-dev