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
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
