[isabelle] A single way to reference AFP entries

[Gerwin Klein]

So I wonder: Is it not possible to device a way that allows the same
theories to work inside the AFP and outside? Why is it that within the
AFP, $AFP cannot be set appropriately (to ".." if you want)?

Yes: you place the other AFP entries next to yours in the local directory structure, such that “../Entry/theory” refers to the correct theory.

This is indeed restrictive, because it determines your directory layout (some programming languages force that in any case), but once submitted to the AFP it is probably a good idea to at least keep it in its own isolated directory anyway, and having it organised such that AFP dependencies live next to it does make a certain sense.

I.e. something along the lines of

my-repo/
other-things/
AFP-things/
my-entry/
other-entry1/
other-entry2/

Of course, AFP-things/ could be the root level or anywhere else in your structure, and there could be non-AFP things underneath it as well - this is just an example.

The reason for .. mentioned above is that "it interacts correctly with
multiple AFP installations side by side". But would setting AFP=.., if
one has to work with multiple installations, not do the same?

Unfortunately not. $AFP is set as part of the component setup in the AFP itself - so whichever AFP installation you mention last in the component initialisation setup will be the one $AFP refers to.

Cheers,
Gerwin


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

[Lars Hupel]

So I wonder: Is it not possible to device a way that allows the same
theories to work inside the AFP and outside? Why is it that within the
AFP, $AFP cannot be set appropriately (to ".." if you want)?

There are mostly technical reasons for this, affecting both users and
the testing infrastructure. Gerwin has already explained the former.

The effect on the testing infrastructure is that building the AFP would
require component setup, which is problematic when paths are not known.
Isabelle would need to be aware of concrete paths of things on the build
servers (which are not constant).

[Makarius]

What could and should changed, either in Isabelle or the AFP component
setup, so that it _becomes_ possible to use the theories in both setups
(within the AFP directory structure, as well as stand-alone theories
using the registered AFP component)?

Certain reforms about locating theory sources via the formal session
structure have been in the pipeline for several years. I hope to get
that through before every release, and still do hope so for the one in
autumn 2016.

The general principle is that theories are no longer addressed via
file-system locations, but by logical names that stem from the
collective session definitions that are presently active. The main
mechanism to vary that session context is what you see as option -d in
"isabelle build" or "isabelle jedit", or the "dirs" in Isabelle/Scala
interfaces.

Lets see what comes out of that, when we are finally standing there.
Stay tuned and keep an eye on isabelle-dev ...


Makarius

[Lars Hupel]

Post by Gerwin Klein

The reason for .. mentioned above is that "it interacts correctly
with multiple AFP installations side by side". But would setting
AFP=.., if one has to work with multiple installations, not do the
same?

Unfortunately not. $AFP is set as part of the component setup in the
AFP itself - so whichever AFP installation you mention last in the
component initialisation setup will be the one $AFP refers to.

In consequence, this would also mean that AFP couldn't be used without
installing it (i.e. registering as a component).