[isabelle-dev] Modest proposal for image tagging

[Rafal Kolanski]

Dear Isabelle Developers,

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.

An approach:

Now, Makarius will doubtless tell me I've done it wrong, but within our 
project I have added a global "val image_identifier" string in every 
image which at least has the name of the image, along with any other 
identifying features. Then I added the "-I" option to isabelle usedir 
which allows one to specify those identifying features. I then modified 
wwwfind to display this string in the title.

So for example, when we build one of our images, we use:
IMAGE_IDENTIFIER_TAG = `hg log -l 1 --template '{node} {date|isodate}\n' 
-r .`
USEDIR = $(ISABELLE_TOOL) usedir -v true -i false -d false -I 
"$(IMAGE_IDENTIFIER_TAG)"

Then if we connect to our wwwfind server on a given port, the title reads:
Find Theorems: CREFINE (7a95fca6ca33e071fd1c948a559898af7e21697e 
2011-06-24 20:11 +1000)

If we pull the image off the server, we can also get this string by 
evaluating image_identifier.

I think that this style of feature would be really nice in Isabelle. I 
am also attaching a patch for Isabelle 2009-1 for your consideration.

If there is interest, I can port it to 2011, but I'd like to get some 
feedback first.

Sincerely,

Rafal Kolanski.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: isa_image_tag.patch
Type: text/x-patch
Size: 3099 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20110711/7e73dc12/attachment.bin>