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

[Thomas Sewell]

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 <makarius at sketis.net>
Sent: Friday, November 30, 2018 10:18:12 PM
To: Thomas Sewell; Jonathon Fernyhough; isabelle-dev at 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20181204/bc3f6dee/attachment.html>