On 30/11/2018 21:56, Makarius wrote:
> On 30/11/2018 19:45, Thomas Sewell wrote:
>
> 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).
>
> 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/...
Another side-remark: Poly/ML does store an absolute path for the
imported heap hierarchy, but Isabelle/ML ignores that: it uses freshly
resolved file names with PolyML.SaveState.loadHierarchy. Only the
logical session name and the SHA1 key is taken into account for
dependency management.
I've confirmed that with my experiment: using the "strings" tool on the
heap file yields precisely one file name in my own home directory (where
everything was built): it is the (unused) physical heap file name
(before moving the whole installation).
[All of this with official Isabelle2018 -- and all this discussion
properly belongs to the isabelle-users mailing list. There is no mailing
list for "packaging of Isabelle for Linux distributions".]
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
