Email Gateway (Aug 22 2022 at 16:07): Email Gateway (Aug 22 2022 at 16:07):From: Peter Lammich <lammich@in.tum.de>
Isabelle just died with jedit showing the following error:
Welcome to Isabelle/Sepref_IICF (Isabelle2017-RC2: September 2017)
Run out of store - interrupting threads
Run out of store - interrupting threads
Run out of store - interrupting threads
Run out of store - interrupting threads
Failed to recover - exiting
Failed to recover - exiting
Cannot read message:
Connection reset
message_output terminated
standard_error terminated
standard_output terminated
process terminated
command_input terminated
process_manager terminated
Return code: 1
Apart from the image of the base session, Sepref_IICF from AFP, there
where only a few files loaded. That never happened to me with Isabelle
before.
Email Gateway (Aug 22 2022 at 16:07):From: Peter Lammich <lammich@in.tum.de>
Update: This seems to be reproducible, so it's currently a SHOWSTOPPER
for me using Isabelle2017. I'm now looking for a publically accessible
example ...
Email Gateway (Aug 22 2022 at 16:07):From: Makarius <makarius@sketis.net>
What are your settings for Poly/ML? (E.g. via "isabelle build -?")
You have the largest sessions in AFP concerning heap size, so it is
likely that ML_system_64 is now required.
Makarius
Email Gateway (Aug 22 2022 at 16:07):From: Peter Lammich <lammich@in.tum.de>
What are your settings for Poly/ML? (E.g. via "isabelle build -?")
ISABELLE_BUILD_OPTIONS=""
ML_PLATFORM="x86-linux"
ML_HOME="/home/lammich/opt/Isabelle2016-1/contrib/polyml-5.6-1/x86-
linux"
ML_SYSTEM="polyml-5.6"
ML_OPTIONS="-H 500"
I did not change any of these options.
You have the largest sessions in AFP concerning heap size, so it is
likely that ML_system_64 is now required.
That might be, my poly-process will remain at a bit less than 4G memory
usage with jedit being grayed out for a while, before I get the error
message.
How to activate the 64 bit poly?
Cheers,
Peter
Makarius
Email Gateway (Aug 22 2022 at 16:07):From: Makarius <makarius@sketis.net>
There is a system option called "ML_system_64", it can be changed e.g.
in the Isabelle/jEdit dialog Plugins / Plugin Options / Isabelle /
General / ML System 64. That global state information is stored in
$ISABELLE_HOME_USER/etc/preferences.
A change requires restarting the whole Isabelle application.
Makarius
Email Gateway (Aug 22 2022 at 16:09):From: Peter Lammich <lammich@in.tum.de>
Actually, after finding and fixing the reason for the extensive memory
usage, I can verify the theories also in 32 bit mode.
The real reason was a looping proof method, internally producing bigger
and bigger terms. The looping was introduced by a mistake in my proof,
but has only been triggered by switching from 2016-1 to 2017-RC2, so it
got unnoticed for 2016-1.
Last updated: Apr 20 2024 at 08:16 UTC