Re: [isabelle] Isabelle2016-RC3 -- jEdit build fails when session loaded from different directory

The standard desktop setup is 32GB RAM with a higher-end quadcore i7. This allow you to run 2 sessions in parallel without too much trouble. Without memory pressure it’ll take about 20GB, but with GC it should fit into 16GB (it’s very close to that 16GB limit, sometimes over sometimes under, depending on changes in proofs, Isabelle, polyml, Linux or Mac, etc).

Server side we’re currently running an 8-core i7 with 128GB, but it’s getting a bit old and is in need of a refresh.

Most of the proofs do actually run fine on a 8GB laptop. It’s only the later stages and C-level proofs that need that much memory.


> On 04.02.2016, at 08:24, Matthew Fernandez <Matthew.Fernandez at> wrote:
> On 04/02/16 07:40, Makarius wrote:
>> On Wed, 3 Feb 2016, Matthew Fernandez wrote:
>>> Maybe I'm missing some context for this statement, but why is using 64-bit Poly/ML a mistake? This is what I use and,
>>> as far as I'm aware, is the default configuration in the l4.verified proofs setup [0]. I don't have a deep knowledge
>>> of the Poly/ML implementation but my understanding is that, while the 64-bit version uses more memory to accomplish
>>> the same thing, you *must* use it if you want to use more than N bytes of RAM (for some N; 4GB?).
>> For more than 3 years big Isabelle applications are usually run in constant space of approx. 3.5 GB, i.e. the maximum on
>> 32bit.  This applies to all of Isabelle + AFP, and is usually the most efficient way on small and big machines.
>> Applications that really need more GBs -- presumably l4.verified is the only one on the planet -- there is no other way
>> than to move on to bigger machines and the 64bit model.
>> What kind of hardware do l4.verified people use for that?
> Raf Kolanski can probably provide details about our server, but for my own desktop machine I have an Intel i7 with 32GB
> RAM. On my current proofs I regularly exceed 20GB.
> ________________________________
> 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.