Re: [isabelle] Isabelle2005 proof terms



I just made a settings file with one line:

ISABELLE_USEDIR_OPTIONS="-p 1"

then ran

build HOL

I'm running poly/ML

$ polyml
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%)
Mapping /usr/local/polyml/ML_dbase
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.

Sean

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. 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.


	Makarius







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