Re: [isabelle] Disk usage in ~/.isabelle/contrib



> On 8 Feb 2016, at 10:06 AM, Makarius <makarius at sketis.net> wrote:
>
> On Mon, 8 Feb 2016, Matthew Fernandez wrote:
>
>> You are completely correct, Makarius. I forgot that we (Data61) were using a repository snapshot, rather than a release.
>
>>> Why not use the shrink-wrapped official release? (This is not a
>>> rhetoric question, but the key question on this thread.)
>>
>> Entirely correct.
>
> So what are the reasons for people at Data61 using a repository snapshot?
> I thought that vice had been given up in 2005.
>
> Or is it an official Isabelle release that has been "spiced up" by local patches?

It is precisely that. It just looks like a repository setup for locals.


> In the latter case, I recommend to produce a proper release locally, with a name that is derived from the official one, but different from it. E.g. like this:
>
>  hg tag Isabelle2016-Data61
>  Admin/Release/build -O -r Isabelle2016-Data61

This is difficult from a configuration management point of view. Like in the Isabelle repository itself we want to be able to go back to old versions in history and have a link from our proofs to precisely the Isabelle version (change id, including any spice) and configuration that was applicable there. Itâs also very useful to have the Isabelle repository directly there, to be able to study history, and to manage any additional spice as version-controlled branches.

This means we effectively deal with a Isabelle repository setup. Iâm happy with that trade-off, but some of us are more perfectionist ;-) I think with the information so far, we can optimise our setup, though.


> This works in Linux and Mac OS X (e.g. Mountain Lion), but the latter is required to produce macos bundles.  Linux can produce only linux and windows bundles, and the fonts of documentation is bad, because Gerwin and Tobias like strange fonts.

Interesting. Do you mean the Concrete Maths font? I havenât had any issues with it so far.

Cheers,
Gerwin


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.