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