[isabelle-dev] Modest proposal for image tagging
makarius at sketis.net
Tue Jul 12 12:01:01 CEST 2011
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.)
More information about the isabelle-dev