Email Gateway (Aug 17 2022 at 13:45): Email Gateway (Aug 17 2022 at 13:45):From: Sean McLaughlin <seanmcl@cmu.edu>
Hello,
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, I think there's
something wrong.
Any ideas?
Thanks,
Sean
Email Gateway (Aug 17 2022 at 13:45):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 17 2022 at 13:45):From: Makarius <makarius@sketis.net>
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.
Makarius
Email Gateway (Aug 17 2022 at 13:45):From: Sean McLaughlin <seanmcl@cmu.edu>
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
Email Gateway (Aug 17 2022 at 13:45):From: Makarius <makarius@sketis.net>
What exactly is your OS/HW platform? Maybe we should report this also to
polyml-devel, or David Matthews directly.
Makarius
Email Gateway (Aug 17 2022 at 13:45):From: Christoph Lüth <cxl@informatik.uni-bremen.de>
Makarius wrote:
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...
--Christoph.
Last updated: May 03 2024 at 04:19 UTC