Re: [isabelle] Isabelle2005 proof terms
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
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