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.



From: Makarius <makar...@sketis.net>
Sent: Friday, November 30, 2018 10:18:12 PM
To: Thomas Sewell; Jonathon Fernyhough; 
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".]

isabelle-dev mailing list

Reply via email to