Re: [isabelle] Insufficient memory when building heap image



Hallo,

thanks for the quick reply, I should probably give the new PolyML a try
then.

However, I do not quite understand what you mean with this:

> Traditionally, Proof General runs things with slightly different
> options, such as quick_and_dirty and reduced parallel proof checking,
> so there can be easily a difference to batch mode.
>
> I am trying hard not to repeat these mistakes [...]

In my case, loading everything in Proof General works, loading
everything in batch mode does not work. Based on that, I would argue
that whatever options Proof General does run things with are a good
idea, not a mistake. Therefore, I cannot quite follow your reasoning here.


Cheers,
Manuel



On 28/09/12 16:45, Makarius wrote:

> Traditionally, Proof General runs things with slightly different
> options, such as quick_and_dirty and reduced parallel proof checking,
> so there can be easily a difference to batch mode.
>
> I am trying hard not to repeat these mistakes




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