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
