*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] Isabelle2005 proof terms*From*: Sean McLaughlin <seanmcl at cmu.edu>*Date*: Fri, 13 Jan 2006 09:52:25 -0500*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <Pine.LNX.4.58.0601131208500.17764@atbroy65.informatik.tu-muenchen.de>*References*: <09A12887-8877-48D9-85D2-9EB33D3B6FDC@cmu.edu> <Pine.LNX.4.58.0601131208500.17764@atbroy65.informatik.tu-muenchen.de>

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 gigabyteCan you be a little more specific what you've compiled exactly.Are thesejust Isabelle/Pure and HOL, or further theories, i.e. your ownapplication? Is this Poly/ML or SML/XL? Roughly speaking,Isabelle2005uses about half of the resources of Isabelle2004, both space and time. Makarius

**Follow-Ups**:**Re: [isabelle] Isabelle2005 proof terms***From:*Makarius

**References**:**[isabelle] Isabelle2005 proof terms***From:*Sean McLaughlin

**Re: [isabelle] Isabelle2005 proof terms***From:*Makarius

- Previous by Date: [isabelle] Export of proofs from Isabelle in "fully-expanded" form
- Next by Date: Re: [isabelle] Isabelle2005 proof terms
- Previous by Thread: Re: [isabelle] Isabelle2005 proof terms
- Next by Thread: Re: [isabelle] Isabelle2005 proof terms
- Cl-isabelle-users January 2006 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list