Re: [isabelle-dev] Support in `isabelle build` for SOURCE_DATE_EPOCH
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 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
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
Re: [isabelle-dev] Support in `isabelle build` for SOURCE_DATE_EPOCH
On 30/11/2018 19:45, Thomas Sewell wrote: > I'd just like to confirm that other users have seen this issue. > Colleagues of mine > > have tried to pre-build heaps on a build server and share them with other > users. It could have saved CPU-hours, and in some cases, hours of humans > waiting around, but it never worked. > > My understanding is that the "hash the world" mechanism for capturing > the state of the dependencies sometimes captures the absolute names of > files. > This breaks down in the obvious way if, for instance, we can't assume > that all > the target users have the same username. None of this has anything to do > with the archive format. 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). The starting point was about the HOL image, where movable images should work under normal circumstances (I've just tried that a few hours ago). But having a build-server for HOL is usually pointless, because it merely requires 2-5min to build on the spot (and much slower hardware is unusable for Isabelle applications). 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/... I can't say for sure about images outside Isabelle + AFP, but I've occasionally heard about users managing even that (e.g. IsaFoR in Innsbruck). Maybe this was based on a homogeneous file-system layout. Of course, there can be many other ways in user-space to refer persistently to physical file locations, or to build other non-portable information into the heap. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Support in `isabelle build` for SOURCE_DATE_EPOCH
I'd just like to confirm that other users have seen this issue. Colleagues of mine have tried to pre-build heaps on a build server and share them with other users. It could have saved CPU-hours, and in some cases, hours of humans waiting around, but it never worked. My understanding is that the "hash the world" mechanism for capturing the state of the dependencies sometimes captures the absolute names of files. This breaks down in the obvious way if, for instance, we can't assume that all the target users have the same username. None of this has anything to do with the archive format. These observations may all be out of date. Cheers, Thomas. From: isabelle-dev on behalf of Makarius Sent: Friday, November 30, 2018 7:13:36 PM To: Jonathon Fernyhough; isabelle-...@mail46.informatik.tu-muenchen.de Subject: Re: [isabelle-dev] Support in `isabelle build` for SOURCE_DATE_EPOCH On 30/11/2018 18:56, Jonathon Fernyhough wrote: >> >>> However, a Debian packaging file is the correct approach for local >>> deployment to multiple Debian/Ubuntu machines. >> >> It is one approach, but typically causes problems. > > Given the size of the Debian repositories and the range of software they > make available I'm not really sure this is true. Hopefully this is not another attempt at an official Debian package of Isabelle. Many years ago, some people tried it, but it always caused more problems than it solved. And today the system is more complex and more easily destroyed by packaging it. These days I see big and complex products doing it our way: providing a fully integrated distribution for end-users that by-passes OS package managers. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Support in `isabelle build` for SOURCE_DATE_EPOCH
On 30/11/2018 18:56, Jonathon Fernyhough wrote: >> >>> However, a Debian packaging file is the correct approach for local >>> deployment to multiple Debian/Ubuntu machines. >> >> It is one approach, but typically causes problems. > > Given the size of the Debian repositories and the range of software they > make available I'm not really sure this is true. Hopefully this is not another attempt at an official Debian package of Isabelle. Many years ago, some people tried it, but it always caused more problems than it solved. And today the system is more complex and more easily destroyed by packaging it. These days I see big and complex products doing it our way: providing a fully integrated distribution for end-users that by-passes OS package managers. Makarius signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Support in `isabelle build` for SOURCE_DATE_EPOCH
On 30/11/2018 16:36, Makarius wrote: > On 30/11/2018 16:30, Jonathon Fernyhough wrote: >> On 30/11/2018 14:55, Makarius wrote: >>> On 30/11/2018 14:15, Jonathon Fernyhough wrote: I'm currently packaging Isabelle2018 (in deb format) for deployment to several machines. These packages should contain some default heaps so users can get on with what they're doing and avoid duplicating hundreds of megabytes of data across user profiles. I'm trying to automate the heap build process using the debian/rules file in the "standard" way but the generated heaps are seen as out-of-date when the user runs the Isabelle GUI, which then tries to regenerate the heaps (and fails because the system directory isn't writable). >>> >>> There is no point do "debianize" Isabelle: it is a plain user-space >>> application program, not a system component. >>> >> >> You're correct that there's no need to do this if you're a single user >> running Isabelle on a single machine. > > Isabelle dates back from a time of multi-user / multi-platform > installations, although that is rarely used these days. This scheme > still works. It is even more general than Debianization. > > >> However, a Debian packaging file is the correct approach for local >> deployment to multiple Debian/Ubuntu machines. > > It is one approach, but typically causes problems. Given the size of the Debian repositories and the range of software they make available I'm not really sure this is true. >>> You should be able to achive the above without deb packaging like this: >>> >>> * unpack the Isabelle tar.gz >>> * run "Isabelle/bin/isabelle build -s -b HOL" (or any other images >>> that users might need) >>> * copy the result to the target (e.g. via "cp -a" or as a tar.gz) >>> >>> Here "Isabelle" refers to any Isabelle distribution from recent years: >>> it is normal that Isabelle users have more than one of it active. >> >> I suppose that would be a workaround - build the heaps as part of >> packaging process but archive them, then extract them during installation. > > Isn't this the normal way of packaging build artifacts? I meant that the heaps could be built but included as a vendored archive rather than included as bare files in the package. An archive-in-an-archive, if you will. >>> Also note that "isabelle build" uses SHA1 hash keys on the sources, not >>> datestamps. >> >> This raises a different question of why the **sources** SHA1 hashes are >> different between the packaging chroot (pbuild/sbuild) and the local system. >> >> What is being hashed? A full path or just the filename? > > Just the content of everything that is required: sources, other heaps etc. > > There is one side-condition: the file-system needs to be reasonably sane > to allow folding file names back to the symbolic form of ~~/src/HOL/ROOT > etc. -- my guess it that the funny Debian build environment somehow > destroys that. > OK, I'll have a dig into the behaviour of the Isabelle tools to see how they interact with the filesystem. Something is doing something odd somewhere along the line. > (BTW: nothing of this is relevant to the isabelle-dev mailing list.) > Apologies. I'll take this elsewhere. J signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Support in `isabelle build` for SOURCE_DATE_EPOCH
On 30/11/2018 16:30, Jonathon Fernyhough wrote: > On 30/11/2018 14:55, Makarius wrote: >> On 30/11/2018 14:15, Jonathon Fernyhough wrote: >>> >>> I'm currently packaging Isabelle2018 (in deb format) for deployment to >>> several machines. These packages should contain some default heaps so >>> users can get on with what they're doing and avoid duplicating hundreds >>> of megabytes of data across user profiles. >>> >>> I'm trying to automate the heap build process using the debian/rules >>> file in the "standard" way but the generated heaps are seen as >>> out-of-date when the user runs the Isabelle GUI, which then tries to >>> regenerate the heaps (and fails because the system directory isn't >>> writable). >> >> There is no point do "debianize" Isabelle: it is a plain user-space >> application program, not a system component. >> > > You're correct that there's no need to do this if you're a single user > running Isabelle on a single machine. Isabelle dates back from a time of multi-user / multi-platform installations, although that is rarely used these days. This scheme still works. It is even more general than Debianization. > However, a Debian packaging file is the correct approach for local > deployment to multiple Debian/Ubuntu machines. It is one approach, but typically causes problems. >> You should be able to achive the above without deb packaging like this: >> >> * unpack the Isabelle tar.gz >> * run "Isabelle/bin/isabelle build -s -b HOL" (or any other images >> that users might need) >> * copy the result to the target (e.g. via "cp -a" or as a tar.gz) >> >> Here "Isabelle" refers to any Isabelle distribution from recent years: >> it is normal that Isabelle users have more than one of it active. > > I suppose that would be a workaround - build the heaps as part of > packaging process but archive them, then extract them during installation. Isn't this the normal way of packaging build artifacts? >> Also note that "isabelle build" uses SHA1 hash keys on the sources, not >> datestamps. > > This raises a different question of why the **sources** SHA1 hashes are > different between the packaging chroot (pbuild/sbuild) and the local system. > > What is being hashed? A full path or just the filename? Just the content of everything that is required: sources, other heaps etc. There is one side-condition: the file-system needs to be reasonably sane to allow folding file names back to the symbolic form of ~~/src/HOL/ROOT etc. -- my guess it that the funny Debian build environment somehow destroys that. (BTW: nothing of this is relevant to the isabelle-dev mailing list.) Makarius signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Support in `isabelle build` for SOURCE_DATE_EPOCH
On 30/11/2018 14:55, Makarius wrote: > On 30/11/2018 14:15, Jonathon Fernyhough wrote: >> >> I'm currently packaging Isabelle2018 (in deb format) for deployment to >> several machines. These packages should contain some default heaps so >> users can get on with what they're doing and avoid duplicating hundreds >> of megabytes of data across user profiles. >> >> I'm trying to automate the heap build process using the debian/rules >> file in the "standard" way but the generated heaps are seen as >> out-of-date when the user runs the Isabelle GUI, which then tries to >> regenerate the heaps (and fails because the system directory isn't >> writable). > > There is no point do "debianize" Isabelle: it is a plain user-space > application program, not a system component. > You're correct that there's no need to do this if you're a single user running Isabelle on a single machine. However, a Debian packaging file is the correct approach for local deployment to multiple Debian/Ubuntu machines. Yes, you could deploy to a network file store, but then you're transferring hundreds of megabytes on startup to every machine which runs the software - which is the same issue if your user profile is on a network file store and the exact thing I'm trying to avoid. > You should be able to achive the above without deb packaging like this: > > * unpack the Isabelle tar.gz > * run "Isabelle/bin/isabelle build -s -b HOL" (or any other images > that users might need) > * copy the result to the target (e.g. via "cp -a" or as a tar.gz) > > Here "Isabelle" refers to any Isabelle distribution from recent years: > it is normal that Isabelle users have more than one of it active. I suppose that would be a workaround - build the heaps as part of packaging process but archive them, then extract them during installation. > Also note that "isabelle build" uses SHA1 hash keys on the sources, not > datestamps. This raises a different question of why the **sources** SHA1 hashes are different between the packaging chroot (pbuild/sbuild) and the local system. What is being hashed? A full path or just the filename? J signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Support in `isabelle build` for SOURCE_DATE_EPOCH
On 30/11/2018 14:15, Jonathon Fernyhough wrote: > > I'm currently packaging Isabelle2018 (in deb format) for deployment to > several machines. These packages should contain some default heaps so > users can get on with what they're doing and avoid duplicating hundreds > of megabytes of data across user profiles. > > I'm trying to automate the heap build process using the debian/rules > file in the "standard" way but the generated heaps are seen as > out-of-date when the user runs the Isabelle GUI, which then tries to > regenerate the heaps (and fails because the system directory isn't > writable). There is no point do "debianize" Isabelle: it is a plain user-space application program, not a system component. You should be able to achive the above without deb packaging like this: * unpack the Isabelle tar.gz * run "Isabelle/bin/isabelle build -s -b HOL" (or any other images that users might need) * copy the result to the target (e.g. via "cp -a" or as a tar.gz) Here "Isabelle" refers to any Isabelle distribution from recent years: it is normal that Isabelle users have more than one of it active. Also note that "isabelle build" uses SHA1 hash keys on the sources, not datestamps. Makarius signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Support in `isabelle build` for SOURCE_DATE_EPOCH
Hi! I'm currently packaging Isabelle2018 (in deb format) for deployment to several machines. These packages should contain some default heaps so users can get on with what they're doing and avoid duplicating hundreds of megabytes of data across user profiles. I'm trying to automate the heap build process using the debian/rules file in the "standard" way but the generated heaps are seen as out-of-date when the user runs the Isabelle GUI, which then tries to regenerate the heaps (and fails because the system directory isn't writable). If I generate the heaps in a postinst script it works as expected, though this isn't very efficient as the heaps will be generated on many "slow" machines instead of just once on a "fast" machine. I think this all comes down to the Reproducible Builds efforts [1]. During the package build process, all timestamps are overridden with the environment variable SOURCE_DATE_EPOCH [2]. If "real" timestamps are being recorded in the heap generation log database [3] then the packaged timestamps will not match the logged timestamps. If this is the cause, I'd like to request that `isabelle build` uses the variable SOURCE_DATE_EPOCH (when set) to determine file timestamps. Best, Jonathon [1] https://wiki.debian.org/ReproducibleBuilds/Howto [2] https://reproducible-builds.org/specs/source-date-epoch/ [3] https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2013-September/msg00143.html signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
