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 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
[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
