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
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev