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