On 30/11/2018 19:45, Thomas Sewell wrote:
> I'd just like to confirm that other users have seen this issue.
> Colleagues of mine
>
> have tried to pre-build heaps on a build server and share them with other
> users. It could have saved CPU-hours, and in some cases, hours of humans
> waiting around, but it never worked.
>
> My understanding is that the "hash the world" mechanism for capturing
> the state of the dependencies sometimes captures the absolute names of
> files.
> This breaks down in the obvious way if, for instance, we can't assume
> that all
> the target users have the same username. None of this has anything to do
> with the archive format.
I am also unsure why "archive formats" got on this thread. The heap is a
binary build artifact, with its own internal structure. Its precise
content is somewhat non-deterministic, even when everything runs in
sequential mode (which is very slow and hardly ever done).
The starting point was about the HOL image, where movable images should
work under normal circumstances (I've just tried that a few hours ago).
But having a build-server for HOL is usually pointless, because it
merely requires 2-5min to build on the spot (and much slower hardware is
unusable for Isabelle applications).
It works due to some special trickery for the main Isabelle sessions
(and in Isabelle2018 also for AFP) via Path.smart_implode, to fold
physical file locations back into symbolic form: $ISABELLE_HOME/src/...
or $AFP/...
I can't say for sure about images outside Isabelle + AFP, but I've
occasionally heard about users managing even that (e.g. IsaFoR in
Innsbruck). Maybe this was based on a homogeneous file-system layout.
Of course, there can be many other ways in user-space to refer
persistently to physical file locations, or to build other non-portable
information into the heap.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
