Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] problem with the last development snapshot

view this post on Zulip Email Gateway (Aug 18 2022 at 10:49):

From: Temesghen Kahsai <lememta@gmail.com>
Hi all,

I m trying to install the last development snapshot of Isabelle.
Somehow I get the following error:

Started at Thu Sep 20 17:44:31 BST 2007 (polyml-4.1.4_ppc-darwin on
cslttk.swan.ac.uk)
Building Pure ...
Finished Pure (0:00:55 elapsed time, 0:00:34 cpu time)
Building HOL ...
Run out of store - interrupting console processes
HOL FAILED
(see also /usr/local/share/Isabelle_20-Sep-2007/heaps/
polyml-4.1.4_ppc-darwin/log/HOL)

(bstring * xstring * bool) list ->
Context.theory * Thm.thm -> Context.theory * Thm.thm
val quiet_mode : bool ref
end
structure SpecificationPackage : SPECIFICATION_PACKAGE
Loading theory "ATP_Linkup" (required by "Main" via "Map" via "List"
via "PreList")
*** Interrupt.
*** At command "theory" (line 9 of "/usr/local/share/Isabelle_20-
Sep-2007/src/HOL/ATP_Linkup.thy").
*** Error in ROOT.ML
*** Exception- TOPLEVEL_ERROR raised

make: *** [/usr/local/share/Isabelle_20-Sep-2007/heaps/
polyml-4.1.4_ppc-darwin/HOL] Error 1

Any advice?

Thanks.

Teme

view this post on Zulip Email Gateway (Aug 18 2022 at 10:49):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hmmm... does the problem re-occur on re-building? It seems to be a
non-functional issue.

Florian
florian.haftmann.vcf

view this post on Zulip Email Gateway (Aug 18 2022 at 10:49):

From: Stefan Berghofer <berghofe@in.tum.de>
Temesghen Kahsai wrote:
Hi Temesghen,

you should try to upgrade to PolyML 5.0. Some older versions of PolyML have
problems handling applications that consume a large amount of heap space.
You also have to make sure that the default maximum heap size for PolyML
is set to the right value, but this should be taken care of by the default
Isabelle settings file automatically.

Greetings,
Stefan

view this post on Zulip Email Gateway (Aug 18 2022 at 10:50):

From: Makarius <makarius@sketis.net>
It seems that Isabelle/HOL has recently grown too fat for Poly/ML 4.x on
ppc, which uses slightly more memory than x86 so we did not notice yet.

Luckily Poly/ML 5.0 is reasonably stable for production use right now,
although it can also run into situations where the stack cannot be
increased despite plenty of free memory being available.

The still emerging Poly/ML 5.1 (available via CVS) won't have any of these
problems and you can already play around with multicore machines right
now.

See http://www.polyml.org/download.html for further details.

Makarius

Last updated: May 03 2024 at 01:09 UTC