[isabelle-dev] Modest proposal for image tagging

[Makarius]

On Tue, 12 Jul 2011, Rafal Kolanski wrote:

> 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.

This sounds like the regression test server merely needs to use the result 
of "isabelle version -i" as part of the filesystem location, and maybe 
produce some symlink "latest -> ..." in the end.

I don't understand why this information needs to be in the binary. 
Strictly speaking, loading the image aleady requires to know which version 
of Isabelle (and Poly/ML) is used -- although there is in practice some 
tolerance of several months until things really break. (This happens when 
bisecting over really ancient versions, for example.)


 	Makarius