[isabelle-dev] Modest proposal for image tagging

[Makarius]

On Mon, 11 Jul 2011, Rafal Kolanski wrote:

> The problem:
>
> There exist situations whereupon we find ourselves with an Isabelle image 
> file without knowing what exactly it is.
>
> One such situation is using wwwfind to present multiple images on multiple 
> ports. One cannot expect users to remember which is which just based on the 
> port number. It is much more useful to have the image name in the title.
>
> Combined with a regression test system which automatically refreshes such 
> images, it is also pertinent to know which repository revision the particular 
> image was built from. This is also true when copying images between machines 
> that would normally take hours to build (e.g. grabbing them from the 
> regression test server in the morning).
>
> Isabelle (well, the normal release one) currently does not have such a 
> feature.

Have you seen structure Distribution in the ML context?  The 
Session.welcome message is also based on that.  WWW_Find just needs to 
provide this information to the client.

Concerning confusion of image files etc., it is basically your job to 
organize them in directories such that others find them again.  The 
standard settings of official releases or snapshots already include the 
ISABELLE_IDENTIFIER as directory prefix for ISABELLE_HOME_USER.  Other 
directory schemes can be done similarly in user space.

No tagging like that happens when you have a private repository clone, 
though.  By definition, private things are not shared with others, so 
there is no confusion. (Nonetheless there is isabelle version -i to tell 
about local repository state in the manner of Mercurial, with optional "+" 
signs etc. to indicate uncommitted stuff.)


BTW, I am currently "formalizing" many aspects of Isabelle management of 
system resources (images etc.) by producing official Isabelle/Scala 
library functions.  After some initial uncertainty, it has become clear 
that there is an implicit assumption that all contributing parts are from 
exactly the same Isabelle version.  In general, you cannot have robust 
tools that work with images from other versions, so no attempt is made in 
that direction.


 	Makarius