Re: [isabelle] Isabelle2005 proof terms

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/ML 4.1.3 has some known issues in this respect. You may want to try the precompiled binaries from the Isabelle distribution page, which are with -p 2 for HOL and use Poly/ML 4.1.4 as included.

Following on from this, I'm experiencing related (?) problems here: if I try to build Isabelle2005 with proof objects under Poly/ML 4.2.0, it fails with

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

I tried running discgarb on the Pure database before building HOL, and I also tried creating a child database from Pure to build HOL with (as suggested by the Poly/ML FAQ). but to no effect. (I'm using PolyML-4.2.0 and Isabelle 2005, with the database patched using the polyml-4.1.4-patch.ML from the repository.) This only happens with PolyML 4.2.0, 4.1.3 builds perfectly (but does not run on all machines).

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


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