Re: [isabelle] Isabelle2005 proof terms

On Thu, 12 Jan 2006, Sean McLaughlin wrote:

> I upgraded today to Isabelle2005 and tried to compile the proof terms
> with both the -p 1 and -p 2 options, as I did with Isabelle2004.  It
> runs for some hours and builds files of over 40 GB.  As the heaps for
> Isabelle2004 were less than a gigabyte

Can you be a little more specific what you've compiled exactly.  Are these
just Isabelle/Pure and HOL, or further theories, i.e. your own
application?  Is this Poly/ML or SML/XL?  Roughly speaking, Isabelle2005
uses about half of the resources of Isabelle2004, both space and time.


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