Re: [isabelle] Isabelle2005 proof terms
I just made a settings file with one line:
I'm running poly/ML
Poly/ML RTS version PPC-4.1.3 (12:05:53 09/23/02)
Copyright (c) 2002 CUTS and contributors.
Running with heap parameters (h=10240K,ib=2048K,ip=100%,mb=6144K,mp=20%)
Poly/ML 4.1.3 Release
Just the Pure theory alone took 18 minutes to build and was
multiple gigabytes. When I did this before with Isabelle2004 it
was only 10MB. (22 MB using sml/nj)
Any ideas? This is very strange.
On Jan 13, 2006, at 6:12 AM, Makarius wrote:
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.
just Isabelle/Pure and HOL, or further theories, i.e. your own
application? Is this Poly/ML or SML/XL? Roughly speaking,
uses about half of the resources of Isabelle2004, both space and time.
This archive was generated by a fusion of
Pipermail (Mailman edition) and