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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
