[isabelle-dev] Support in `isabelle build` for SOURCE_DATE_EPOCH

[Makarius]

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