[isabelle-dev] Modest proposal for image tagging

[Alexander Krauss]

Hi Rafal,

> If the entire team and the regression test server are using the *same*
> isabelle version, then for a given image file, which repository revision
> does it correspond to?
> For example, my twice-daily regression scripts just completed 1.5 hours
> ago and the next full test is at noon. If someone comes in to work at
> 9am they can just take those images from the regression test server
> without building them themselves.
>
> There is a slight complication though. One of the images is currently
> failing, which means that that image on the regression test server is
> older than the ones which did build tonight.
> Which is nice, as someone can just grab *that* and quickly start working
> with the last working version. We also don't want wwwfind to just die
> and give us nothing, but rather search the last working version.
> Then the question is which revision was that generated from? Oh and from
> when is that?

This is clearly a very useful setup, but things like this should not 
invade the fundamentals of the system. The semantics of concepts like 
"session" have been a bit unclear in the past (we are hoping that this 
becomes better now). Adding new features here wouldn't help.

You can easily achieve your goal without having to hack yourself into 
session management. Here are two ideas:

A) In the build process, before the invocation of isabelle usedir, paste 
the output of "hg id" (or similar) into some source file, e.g.,

version.ML:

   val build_version = "THE_VERSION";

IsaMakefile:


   sed -i 's/THE_VERSION/$(hg id)/g' version.ML
   isabelle usedir ...

Actually, a similar thing happens when an isabelle distribution is built 
from a repository clone.


B) Keep metadata as metadata: Your build process stores the image under 
a directory/filename that contains the version information. WWWfind can 
take this into account either by inspecting the file name or via an 
extra parameter. Actually, the administration of log files in 
traditional isatest works like this.

I'm sure you'll have even more ideas when you think about it a bit more...

Alex