*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] Isabelle2005 proof terms*From*: Christoph Lüth <cxl at informatik.uni-bremen.de>*Date*: Mon, 16 Jan 2006 00:34:52 +0100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <Pine.GSO.4.60.0601131936400.10997@sunbroy2.informatik.tu-muenchen.de>*References*: <09A12887-8877-48D9-85D2-9EB33D3B6FDC@cmu.edu> <Pine.LNX.4.58.0601131208500.17764@atbroy65.informatik.tu-muenchen.de> <B1D7F6BC-B951-4483-B09B-F576A28BBCBA@cmu.edu> <Pine.GSO.4.60.0601131936400.10997@sunbroy2.informatik.tu-muenchen.de>*User-agent*: Mozilla Thunderbird 1.0 (X11/20041207)

Makarius wrote:

On Fri, 13 Jan 2006, Sean McLaughlin wrote: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.This is indeed very strange. I've never seen such large Poly/ML images-- actually the system cannot go beyond 500MB for technical reasons.Maybe there is some strangeness in your general system setup, Poly/ML4.1.3 has some known issues in this respect. You may want to try theprecompiled binaries from the Isabelle distribution page, which are with-p 2 for HOL and use Poly/ML 4.1.4 as included.

No more room for pages in database. Try running discgarb.

Strangely. the repository version builds fine with Poly/ML-4.2.0... --Christoph.

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

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

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

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

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

- Previous by Date: Re: [isabelle] Export of proofs from Isabelle in "fully-expanded" form
- Next by Date: [isabelle] proof term request
- 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