Apologies, I forgot about this discussion and just now remembered it.
It sounds like this feature might be quite valuable to projects like l4.verified with fairly "heavy" sessions. I'm not on that project any more, but perhaps someone there will have time to investigate whether everything can be set up so that the right Path.smart_implode events happen, and perhaps whether it's easy to set up a check that this happens. Cheers, Thomas. ________________________________ From: Makarius <makar...@sketis.net> Sent: Friday, November 30, 2018 10:18:12 PM To: Thomas Sewell; Jonathon Fernyhough; isabelle-...@mail46.informatik.tu-muenchen.de Subject: Re: [isabelle-dev] Support in `isabelle build` for SOURCE_DATE_EPOCH 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