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.


Attachment: signature.asc
Description: OpenPGP digital signature

isabelle-dev mailing list

Reply via email to