[isabelle-dev] Modest proposal for image tagging

[Rafal Kolanski]

On 11/07/11 21:24, Makarius wrote:
> 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.

I believe I did not represent what it is used for in sufficient clarity
to avoid a misunderstanding. I'm not talking about tagging the isabelle
version, isabelle repository version, or in fact anything to do with the
isabelle repository. In fact, you'll notice that in the patch I don't
give any extra tags to Pure other than the info that it's the "Pure" image.

What I am talking about is our own repository and custom tags within
images produced from it for the *same* version of isabelle. If someone
somehow uses a different version of isabelle, then that is their problem
and it's their job to rebuild everything.

As you pointed out, my storing the image identifier itself is indeed
unnecessary. After your advice to check out struct Distribution, I
examined what calls it and found Session. Session.name () does indeed
give me a name and a chain of names which led to it.

However, my basic idea is that I believe there should also be an extra
"user defined" tag for an image.

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?

As part of our build process, I encode this info in the image itself in
"val image_identifier". What I should have done is modified the Session
structure to have another value to contain the user-specified info,
which I may well do in the near future, so thank you for that.

Nonetheless, please consider the addition of a user-specified string to
Session when using isabelle usedir via some parameter like the crude way
in the patch I submitted.

I hope this at least clears up what I meant.

Sincerely,

Rafal Kolanski.