Email Gateway (Aug 19 2022 at 15:20): Email Gateway (Aug 19 2022 at 15:20):From: Makarius <makarius@sketis.net>
Apart from a protocol crash, there might be non-termination in the
protocol handler, e.g. because of problems to cancel old command
transactions. Normally the protocol loop is detached from actual
execution, though.
A "PIDE greyout" means that the important assign_update message is not
received, e.g. due to heavy overloading, long GC, or actual breakdown of
the ML side.
I am including a changeset for testing, which produces syslog messages
about the critical protocol phases. This works via the "Syslog" panel,
which is buffered and also restricted in size.
Makarius
ch
Email Gateway (Aug 19 2022 at 15:23):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Makarius,
The greyout happened again (with Isabelle2014-RC3). This time, I had typed
thm $
and placed the cursor at $, then opened Query/Find theorems and searched for simp_implies.
I've attached the activity log and the output of the syslog. The Prover.echo command still
works. There are no exceptions in the shell from which I have started PIDE.
Hope this helps
Andreas
greyout.zip
Email Gateway (Aug 19 2022 at 15:24):From: Makarius <makarius@sketis.net>
Thanks for continued testing.
Looking at the results, I would say there is a deadlock in the main
Document.update operation -- as you have pointed out earlier that the CPU
use of the poly process is 0.
We somehow need to get to the bottom if it. Such problems are sometimes
hardware specific, but if we are lucky it is just a soft mistake in my own
machine room of Isabelle/ML.
Can you just continue testing with threads_trace = "5" in
$ISABELLE_HOME_USER/etc/preferences? You need to edit that file offline,
while Isabelle/jEdit is not running. That option will produce massive
amounts of tracing information for syslog, but while the panel is not
open the performance hit should be bearable. Once the greyout happens
again, you open an instance of the panel and look at the tail end of the
last 100 messages.
Makarius
Email Gateway (Aug 19 2022 at 15:24):From: Makarius <makarius@sketis.net>
That conclusion is actually too quick, because it is in conflict with the
following observation:
The Prover.echo command still works.
On the other hand ...
There are no exceptions in the shell from which I have started PIDE.
but the latter refers to JVM exceptions.
If Prover.echo still works after the greyout, the protocol thread is alive
and not dead-locked. The abrupt end of the syslog after Document.update
could also mean that it just crashed, but then we need to see ML
exceptions on Raw Output. The latter is unbuffered, though. Did you have
Raw Output open before the incident?
Makarius
Email Gateway (Aug 19 2022 at 15:25):From: Makarius <makarius@sketis.net>
Just to make sure here is an example for protocol commands that crash:
ML ‹
Isabelle_Process.protocol_command "error" (fn _ => error "Error");
Isabelle_Process.protocol_command "interrupt" (fn _ => Exn.interrupt ());
›
Now the Scala console within Isabelle/jEdit can invoke them like this:
PIDE.session.protocol_command("error")
PIDE.session.protocol_command("interrupt")
The (unbuffered) result in Raw Output will be like this:
Isabelle protocol command failure: "interrupt"
Interrupt
Isabelle protocol command failure: "error"
Error
So if the Raw Output panel is active in this mysterious PIDE greyout, and
the ML protocol command loop failing, it should be visible there.
One reason for Document.update crashing could be a resource problem, which
leads to implicit interrupt in Poly/ML. Above we see that this is printed
explicitly, unlike in the normal user space error output, since this is
the PIDE machine room.
Makarius
Email Gateway (Aug 19 2022 at 15:25):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Makarius,
I opened Raw Output after the greyout. I'll keep Raw Output open the whole time when I
continue testing.
Andreas
Email Gateway (Aug 19 2022 at 15:25):From: Makarius <makarius@sketis.net>
OK, thanks.
Some more details about jEdit dockables: the instance gets created the
first time you open it in the dock and it remains active while visually
closed; it is detroyed only via explicit undocking. In contrast, a
floating instance exists exactly during the livetime of the visible
window.
Makarius
Email Gateway (Aug 19 2022 at 15:25):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Thanks for the hint. That also explains why sledgehammer aborts a running search when I
change the position of the docked sledgehammer panel (say, from dock at bottom to dock at
right).
Andreas
Email Gateway (Aug 19 2022 at 15:27):From: Makarius <makarius@sketis.net>
Some days ago, I've run myself into a situation of permanent "PIDE
greyout" while editing some ML files within Isabelle/HOL, which
automatically means it is under heavy load, because of the immense size of
that session. This was presumably due to a Document.update protocol crash,
but I did not have the Raw Output panel open to confirm it. The
Prover.echo protocol command still worked afterwards.
For the next release candidate, which will be published later today, I
have made an end to this game: PIDE protocol exceptions will be part of
the buffered syslog channel. Thus they can be retrieved later, in the
rare situations when such a breakdown happens.
Moreover, I have made two rounds through the sources, to see where such a
crash can happen theoretically. I found nothing particular about query
commands, but the protocol for PIDE document "garbage collection" had a
weakness stemming from its first implementation 3 years ago: depending on
timing, it was possible to have the ML process refer to undefined items
and thus crash.
My own crash of ML blob editing fits exactly into this pattern, although I
could not reproduce it systematically. The query crash might be the same
or something different. If something like that ever happens again (after
Isabelle2014-RC4), it is important to preserve the content of the Syslog
panel afterwards and show that to me.
Makarius
Email Gateway (Aug 19 2022 at 15:48):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Makarius,
When I use the Query and Sledgehammer panels heavily, PIDE regularly gets into a state
where the theory text has a grey background, but I cannot get it to resume working any
more (There is also no process running, the CPU is idle). The GUI itself is reactive, but
I cannot get any feedback from Isabelle any more. The Syslog only shows the welcome
message and Raw Output is empty. I then have to shut down jEdit and restart PIDE. I am
afraid that I don't know how to come up with a better description.
My system parameters:
Intel® Core™ i7-3630QM CPU @ 2.40GHz, 16GB memory
Ubuntu 12.04 LTS
ML_PLATFORM="x86-linux"
ML_HOME="/home/andreloc/isabelle/Isabelle2014-RC2/contrib/polyml-5.5.2-1/x86-linux"
ML_SYSTEM="polyml-5.5.2"
ML_OPTIONS="-H 500 --gcthreads 4"
ISABELLE_JAVA_SYSTEM_OPTIONS=-Dfile.encoding=UTF-8 -server
JEDIT_JAVA_OPTIONS=-Xms128m -Xmx3072m -Xss2m
Andreas
Email Gateway (Aug 19 2022 at 15:49):From: Makarius <makarius@sketis.net>
There must have been a protocol crash somewhere at the bottom. The next
time when this happens, there are a few things that can be checked to pin
it down more precisely:
* jEdit menu Utilities / Troubleshooting / Activity Log for JVM
exception traces -- if you run "isabelle jedit" on the command line
there should be information on the terminal as well.
* The following simple test of the ML/Scala protocol handler:
- open Raw Output panel, to make it active before trying anything
- open Console/Scala and emit this command:
PIDE.session.protocol_command("Prover.echo", "test")
The result "test" should appear on raw output. This is the command
loop of the prover process in PIDE wrapping.
Makarius
Email Gateway (Aug 19 2022 at 15:50):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Makarius,
Today, I experienced a PIDE greyout again, this time in Isabelle2014 while running
quickcheck. I've attached the Syslog content and the output of error messages in the
terminal from which I had started Isabelle/jEdit.
Hope this helps in narrowing down the problem,
Andreas
greyout.zip
Email Gateway (Aug 19 2022 at 16:13):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Makarius,
Here is another datapoint in the greyout story with Isabelle2014. The attached syslog ends
with a DUP exception. This time there were no exceptions on the command line. The greyout
happened again while I was using the query panel to find theorems.
My setings are:
JEDIT_JAVA_OPTIONS="-Xms1024m -Xmx4096m -Xss4m"
ML_OPTIONS="-H 500 --gcthreads 4"q
Hope this helps,
Andreas
syslog.zip
Email Gateway (Aug 19 2022 at 16:13):From: Harry Butterworth <heb1001@gmail.com>
I have also been having to occasionally quit and restart Isabelle 2014
jedit when it stops working.
Here is the syslog from the latest problem:
Welcome to Isabelle/HOL (Isabelle2014: August 2014)
poly: gc_mark_phase.cpp:439: virtual void
MTGCProcessMarkPointers::ScanAddressesInObject(PolyObject*, POLYUNSIGNED):
Assertion `baseAddr > (PolyWord)obj && baseAddr < ((PolyWord)obj)+length'
failed.
message_output terminated
/usr/local/Isabelle2014/lib/scripts/run-polyml-5.5.2: line 84: 1645
Aborted (core dumped) "$POLY" -q -i $ML_OPTIONS --eval
"$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$MLTEXT")" --error-exit <
/dev/null
rmdir: failed to remove `/tmp/isabelle-harry1631': Directory not empty
standard_error terminated
standard_output terminated
process terminated
command_input terminated
process_manager terminated
Return code: 134
Email Gateway (Aug 19 2022 at 16:16):From: Makarius <makarius@sketis.net>
(This thread is already quite old, but not forgotten. After several weeks
I am back to normal network connectivity, to make a clean sweep ...)
Do you remember anything specific about the situation? E.g. a very big
message being output, say a large subgoal?
The bash output looks like a stack-overflow in
isabelle.Protocol.clean_message, although the trace is truncated and the
exception header is missing.
The JVM is very unflexible in thread stack management: the value given on
startup is taken for all newly created threads, and cannot be changed at
runtime. This makes it hard to guess right once and for all, and for
everyone.
The Isabelle/jEdit settings have these defaults for heap and stack:
JEDIT_JAVA_OPTIONS="-Xms128m -Xmx1024m -Xss2m"
I am using myself this one on a modest 8GB 64bit machine:
JEDIT_JAVA_OPTIONS="-Xms1024m -Xmx4096m -Xss4m"
Bigger machines should easily afford -Xss8m or more.
Oracle basically ships a Harley-Davidson -- it requires a lot of polishing
and handywork from the power-user.
David Matthews provides more flexibility in Poly/ML: the stack can grow
dynamically to some GBs, but even then it is possible to drive the system
to the limits ...
Makarius
Email Gateway (Aug 19 2022 at 16:16):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Makarius,
On 08/10/14 22:51, Makarius wrote:
Today, I experienced a PIDE greyout again, this time in Isabelle2014 while running
quickcheck. I've attached the Syslog content and the output of error messages in the
terminal from which I had started Isabelle/jEdit.Do you remember anything specific about the situation? E.g. a very big message being
output, say a large subgoal?No, everything was quite small, actually. At that time, I was preparing exercises for the
Isabelle course at ETH, so I just had a single theory file based on HOL/Main, and
quickcheck normally outputs only small counterexamples.
The Isabelle/jEdit settings have these defaults for heap and stack:
JEDIT_JAVA_OPTIONS="-Xms128m -Xmx1024m -Xss2m"
I am using myself this one on a modest 8GB 64bit machine:
JEDIT_JAVA_OPTIONS="-Xms1024m -Xmx4096m -Xss4m"
I had the -Xmx4096m option set before, but I will now also adapt your settings for -Xss
and -Xms. Let's see what happens.
Andreas
Email Gateway (Aug 19 2022 at 16:17):From: Makarius <makarius@sketis.net>
I will keep an eye on the JVM stack, and experiment with bigger values for
a future release.
The memory problem is mainly due to the 32bit limitation of our JVM
bundle, especially for Windows. Of course there is a proper 64bit Java
for that platform, but we don't use it yet.
Makarius
Email Gateway (Aug 19 2022 at 16:24):From: Makarius <makarius@sketis.net>
This is a hard crash of the Poly/ML runtime-system. It has been reported
sporadically since about 1 year, e.g. see
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2013-December/msg00090.html
My impression is that it occurs more often with big application or tight
memory size, e.g. on Windows/Cygwin.
What is the approximative size of your application? What is your OS
platform?
Makarius
http://stop-ttip.org 777,282 people so far
Email Gateway (Aug 19 2022 at 16:24):From: Peter Lammich <lammich@in.tum.de>
With Isabelle-2014 + jedit, I get grayouts every day. Some of them
resolve themselves after a few seconds (up to a minute), one or two
times a day I have to restart the IDE. It's annoying, but you get used
to it :(
When I got such a grayout during an Isabelle tutorial recently, I asked
the students who of them had already experienced such a grayout, and had
to restart. Almost all arms raised immediately!
Email Gateway (Aug 19 2022 at 16:25):From: Joachim Breitner <breitner@kit.edu>
Hi,
thanks for the definition; I’ll pay closer attention to it from now, but
I believe I have experienced this or similar effects when there is a
looping procedure. My usual reaction is to go to the beginning of the
file and change something in the theory header, hoping to reset the
processing. It often works, but that does not mean that I’m not just
cargo-culting :-)
Greetings,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 16:26):From: Makarius <makarius@sketis.net>
On Thu, 20 Nov 2014, Peter Lammich wrote:
With Isabelle-2014 + jedit, I get grayouts every day. Some of them
resolve themselves after a few seconds (up to a minute), one or two
times a day I have to restart the IDE. It's annoying, but you get used
to it :(
Getting used to problems means they are likely to remain indefinitely.
It is important that users invest a minimum of time to figure out what is
actually the situation and provide useful feedback on that.
I can only repeat that I am not aware of any such open problems in
Isabelle2014. I need tangible reports to do anything to increase the
general system quality again one step further.
Informal definition of "grayout": The text in the proof buffer becomes
gray, and the prover is not responding any more. You can still edit the
text.
This is correct, and just a normal consequence how PIDE works: the editor
is always ready to accept edits, and sends them continously to the prover.
The prover reports eventually on the results.
The aspect "not responding any more" is a delicate one. For example,
garbage collection on the ML side or overloading with many long-running
tasks could lead to seconds of delay, sometimes half a minute. This is
normal and not an immediate problem. The situation can be improved by
using an adequate machine (e.g. 4 cores and 8 GB is very little by today's
standards).
Actual breakdown of the prover process is something else. The Syslog
panel should show ML exeptions if anything like that has happened. By
showing me that, I can figure out more. By keeping the information
secret, chances for improvement are much diminished.
Makarius
http://stop-ttip.org 925,412 people so far
Email Gateway (Aug 19 2022 at 16:42):From: Makarius <makarius@sketis.net>
The syslog ultimately says this:
Isabelle protocol command failure: "Document.update"
exception DUP ~5951 raised (line 261 of "General/table.ML")
which refers to Table.update_new.
Looking at the source, I did not find a plausible way how this exception
could have happened -- there are normally handlers to say something more
specific like ERROR "Duplicate command: ~5951".
If you see anything like this again, please tell me about it.
In Isabelle/f4e9bd04e1d5 I have reduced the chances of such low-level DUP
exceptions, although that might not be directly relevant. We should
continue this on isabelle-dev next time.
Makarius
Email Gateway (Aug 19 2022 at 16:42):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Makarius,
These DUP exceptions (with varying values) occur several times a day with Isabelle2014.
They happen when I heavily use find_theorems (with session image HOL-Probability). Most
likely, when I start the search while there is no valid context (e.g., because the current
theory file is part of HOL-Probability or because there is a syntax error), or when I
restart the search while another search is still going on. A week ago, I switched to the
repository version (currently 059ba950a657). Since then I have not experienced any of
these greyouts. I'll let you know on isabelle-dev when they reappear.
Andreas
Email Gateway (Aug 19 2022 at 16:42):From: Makarius <makarius@sketis.net>
On Wed, 19 Nov 2014, Andreas Lochbihler wrote:
These DUP exceptions (with varying values) occur several times a day with
Isabelle2014.
I was not aware of any such problem in the official release. As usual,
problems that are kept secret will remain so over indefinite time.
In Isabelle/f4e9bd04e1d5 I have reduced the chances of such low-level
DUP exceptions, although that might not be directly relevant.
It could be worth trying this tiny change
http://isabelle.in.tum.de/repos/isabelle/rev/f4e9bd04e1d5 on official
Isabelle2014, just by editing $ISABELLE_HOME/src/Pure/General/table.ML
accordingly and rebooting the system.
Makarius
http://stop-ttip.org 911,984 people so far
Email Gateway (Aug 19 2022 at 16:42):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Makarius,
On 19/11/14 11:01, Makarius wrote:
These DUP exceptions (with varying values) occur several times a day with Isabelle2014.
I was not aware of any such problem in the official release. As usual, problems that are
kept secret will remain so over indefinite time.
I did not get these exceptions during the test phase of release candidates, but I was not
working as intensively with Isabelle at that time, either. You cannot complain that I have
not reported this problem with DUP. I just did not want to send you an e-mail every time
the same failure occurs.
In Isabelle/f4e9bd04e1d5 I have reduced the chances of such low-level
DUP exceptions, although that might not be directly relevant.It could be worth trying this tiny change
http://isabelle.in.tum.de/repos/isabelle/rev/f4e9bd04e1d5 on official Isabelle2014, just
by editing $ISABELLE_HOME/src/Pure/General/table.ML accordingly and rebooting the system.
I'll do that, but I cannot promise that I will have time to thoroughly test it during
work. My work now has moved to the repository version and no longer runs with
Isabelle2014, but I have a bunch of other theories that I might get back to some time.
Andreas
Email Gateway (Aug 19 2022 at 16:42):From: Makarius <makarius@sketis.net>
I did not complain. My impression is that the testing of the Isabelle2014
release candidates resulted in a fairly good release.
It is just a reminder to everyone who sees practical relevant problems to
report them. Something that fails at intervals of weeks or months is
merely a fine point (still to be considered eventually). Something that
fails daily is getting in the way of practical work.
But frequent and reliable failure also means it is relatively easy to pin
down and eliminate.
Makarius
Email Gateway (Aug 19 2022 at 16:43):From: Peter Lammich <lammich@in.tum.de>
OK, I recommend to apply the tiny change from
http://isabelle.in.tum.de/repos/isabelle/rev/f4e9bd04e1d5 by editing
Isabelle2014/src/Pure/General/table.ML accordingly, and rebooting (which
will cause an automatic rebuild of logic images).If anything like that happens again, just keep me informed.
Again, a permanent grayout, which did not recover itself. This time,
syslog sais:
Welcome to Isabelle/CAVA_Base (Isabelle2014: August 2014)
Isabelle protocol command failure: "Document.update"
exception Thread "Thread creation failed" raised (line 48 of
"ML-Systems/polyml.ML")
Isabelle protocol command failure: "Document.update"
Undefined document version: -60998
Isabelle protocol command failure: "Document.remove_versions"
Attempt to remove execution version -60993
Email Gateway (Aug 19 2022 at 16:44):From: Peter Lammich <lammich@in.tum.de>
This is what syslog printed on my last grayout, which did not recover
itself:
Welcome to Isabelle/CAVA_Base (Isabelle2014: August 2014)
Isabelle protocol command failure: "Document.update"
exception DUP ~111048 raised (line 261 of "General/table.ML")
Email Gateway (Aug 19 2022 at 16:44):From: Makarius <makarius@sketis.net>
OK, I recommend to apply the tiny change from
http://isabelle.in.tum.de/repos/isabelle/rev/f4e9bd04e1d5 by editing
Isabelle2014/src/Pure/General/table.ML accordingly, and rebooting (which
will cause an automatic rebuild of logic images).
If anything like that happens again, just keep me informed.
Makarius
http://stop-ttip.org 1,015,195 people so far
Email Gateway (Aug 19 2022 at 16:45):From: Makarius <makarius@sketis.net>
A java process with 100% (and a few GB memory) could mean that the
specified heap is full and GC failing to continue properly. This is a
well-known "feature" of the JVM. You need to give more room in advance,
e.g. like this in $ISABELLE_HOME_USER/etc/settings:
JEDIT_JAVA_OPTIONS="-Xms1024m -Xmx4096m -Xss4m"
There are a few more examples in
$ISABELLE_HOME/src/Tools/jEdit/etc/settings -- you need to restart the
application afterwards.
This only refers the "isabelle jedit" command-line tool, or the Linux
toplevel "app" script. For Mac OS X, the Info.plist provides similar JVM
properties. Likewise for Windows in the Isabelle2014.ini file.
Note that the defaults are for a 2-4 GB machine in 32bit mode, where JVM
memory is tight. On Linux or Mac OS X the JVM is usually in 64bit mode,
and bigger heap as above can be easily afforded. On Windows the bundled
JVM is always for 32bit, though, but a 64bit one could be installed
manually, e.g. by replacing the Isabelle2014/contrib/jdk directory.
Makarius
http://stop-ttip.org 1,023,025 people so far
Email Gateway (Aug 19 2022 at 16:46):From: Gottfried Barrow <igbi@gmx.com>
Makarius wrote:
A java process with 100% (and a few GB memory) could mean that the
specified heap is full and GC failing to continue properly. This is a
well-known "feature" of the JVM. You need to give more room in
advance, e.g. like this in $ISABELLE_HOME_USER/etc/settings:
JEDIT_JAVA_OPTIONS="-Xms1024m -Xmx4096m -Xss4m"
I'm not having any big problems, but when I try that with 32-bit Java,
on a PC with 16G of RAM, the PIDE tries to start, but quickly terminates.
...the defaults are for a 2-4 GB machine in 32bit mode, where JVM
memory is tight. ... On Windows the bundled JVM is always for 32bit,
though, but a 64bit one could be installed manually, e.g. by replacing
the Isabelle2014/contrib/jdk directory.
So, I did this:
*) Install the 64-bit JDK:
http://www.oracle.com/technetwork/java/javase/downloads/jdk7-downloads-1880260.html
*) Copy 'C:\Program Files\java\jdk1.7.0_71' to
'Isabelle2014\contrib\jdk\jdk1.7.0_71'
*) Rename 'Isabelle2014\contrib\jdk\x86-cygwin' to 'jdk\x86-cygwin__OLD'
*) Rename 'Isabelle2014\contrib\jdk\jdk1.7.0_71' to 'jdk\x86-cygwin'
I'm using these settings on a PC with 16G of RAM and cheap 8-core AMD
FX-8320:
JEDIT_JAVA_OPTIONS="-Xms4G -Xmx8G -Xss4m"
It's working so far. Thanks for the info.
Regards,
GB
Email Gateway (Aug 19 2022 at 16:46):From: Gottfried Barrow <igbi@gmx.com>
With 64-bit Java it worked out and is working out because I set the
environment with a batch file, and then I start 'isabelle' with a
combination of a batch file and bash file like this:
BATCH:
start /MIN mintty.exe -i /Cygwin-Terminal.ico "%~dp0%~n0.bash"
BASH:
isabelle jedit -l HOL
If I try to use 'Isabelle2014.exe' directly, or us it in a batch file, I
get a window that says, "Error starting Java VM".
It doesn't matter to me, but someone else may need the info to use
64-bit Java.
Regards,
GB
Email Gateway (Aug 19 2022 at 16:46):From: Makarius <makarius@sketis.net>
Indeed. This is actually the main reason why Isabelle on Windows does not
have the 64 bit option yet: the .exe already determines the platform
personality, and it is not possible to switch that later.
Java 8 has a slightly different .exe for applications, but it is also
quite new. Maybe that can be used in the next release.
Makarius
http://stop-ttip.org 1,061,642 people so far
Email Gateway (Aug 19 2022 at 16:54):From: Makarius <makarius@sketis.net>
This might be of concern to David Matthews, the man behind Poly/ML.
I just want to point out, that Isabelle/ML can quite easily cope with a
situation, where Thread.fork may sporadically fail due to resource
problems, in a way where exceptions won't crash the system infrastructure.
It will be done like that in the next Isabelle release.
Until then the same procedure as everytime: tangible problem reports lead
to eventual resolution; non-tangible or secret problems will remain
indefinitely.
Makarius
Email Gateway (Aug 19 2022 at 16:54):From: Peter Lammich <lammich@in.tum.de>
Again the assertion error from the garbage-collector, again from jedit
under heavy load.
This (probably Poly/ML) problem starts to get annyoing ...
Peter
Welcome to Isabelle/HOL (Isabelle2014: August 2014)
poly: gc_mark_phase.cpp:439: virtual void
MTGCProcessMarkPointers::ScanAddressesInObject(PolyObject*,
POLYUNSIGNED): Assertion `baseAddr > (PolyWord*)obj && baseAddr <
((PolyWord*)obj)+length' failed.
message_output terminated
Email Gateway (Aug 19 2022 at 17:00):From: Makarius <makarius@sketis.net>
On Tue, 30 Dec 2014, Peter Lammich wrote:
OK, I recommend to apply the tiny change from
http://isabelle.in.tum.de/repos/isabelle/rev/f4e9bd04e1d5 by editing
Isabelle2014/src/Pure/General/table.ML accordingly, and rebooting (which
will cause an automatic rebuild of logic images).If anything like that happens again, just keep me informed.
Again, a permanent grayout, which did not recover itself.
Thanks for reporting that. As always, it is important for me get an
impression about two things:
(1) What kind of crashes can happen.
(2) The approximate frequency they happen.
In that sense, just keep me informed if you see something like this again.
Anyone else who sees the same or similar breakdowns is welcome to say so,
too.
This time, syslog sais:
Welcome to Isabelle/CAVA_Base (Isabelle2014: August 2014)
Isabelle protocol command failure: "Document.update"
exception Thread "Thread creation failed" raised (line 48 of "ML-Systems/polyml.ML")
Isabelle protocol command failure: "Document.update"
Undefined document version: -60998
Isabelle protocol command failure: "Document.remove_versions"
Attempt to remove execution version -60993
Here I was first distracted by the latter part, which would have been an
integrity problem within the PIDE protocol state, i.e. in my own
department.
The relevant bit is "Thread creation failed", though, which is produced by
the Poly/ML runtime system, when the system function pthread_create fails
(according to libpolyml/processes.cpp). The man page for that function
says about error situations:
EAGAIN Insufficient resources to create another thread, or a system-
imposed limit on the number of threads was encountered. The
latter case may occur in two ways: the RLIMIT_NPROC soft
resource limit (set via setrlimit(2)), which limits the number
of process for a real user ID, was reached; or the kernel's sys‐
tem-wide limit on the number of threads, /proc/sys/ker‐
nel/threads-max, was reached.
We can probably ignore the explicit /proc/sys/kernel/threads-max -- it is
a very high value on my Ubuntu system.
In other words, we are back to the usual guess of insufficient resources
-- unless your application was unexpectedly tiny.
It should be explicitly noted that stack space was already sucessfully
allocated -- there is a different exception for that: "Unable to allocate
thread stack".
Maybe we are slowly moving out of the 32-bit era, but there might be a
completely different reason.
Makarius
Email Gateway (Aug 19 2022 at 17:02):From: Peter Lammich <lammich@in.tum.de>
Here is the next one. Putting Isabelle under heavy load seems not to be
a good idea nowadays :(
A few years ago, Isabelle used to be very stable, even on big stuff ...
Welcome to Isabelle/HOL (Isabelle2014: August 2014)
poly: gc_mark_phase.cpp:439: virtual void
MTGCProcessMarkPointers::ScanAddressesInObject(PolyObject*,
POLYUNSIGNED): Assertion `baseAddr > (PolyWord*)obj && baseAddr <
((PolyWord*)obj)+length' failed.
Malformed message:
bad chunk (unexpected EOF after 3012 of 4431 bytes)
message_output terminated
/home/lammich/opt/Isabelle2014/lib/scripts/run-polyml-5.5.2: line 84:
7861 Aborted (core dumped) "$POLY" -q -i $ML_OPTIONS
--eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$MLTEXT")"
--error-exit < /dev/null
standard_error terminated
standard_output terminated
process terminated
command_input terminated
process_manager terminated
Return code: 134
Email Gateway (Aug 19 2022 at 17:03):From: Makarius <makarius@sketis.net>
On Fri, 9 Jan 2015, Peter Lammich wrote:
Here is the next one. Putting Isabelle under heavy load seems not to be
a good idea nowadays :(A few years ago, Isabelle used to be very stable, even on big stuff ...
This impression is not based on facts: the applications today are much
larger than in the past, and we are actually doing quite well.
There was always a hidden concrete wall, and some applications / users
have driven very fast towards it without being aware of normal resource
limitations on concrete computing infrastructure. That concrete wall has
been moved many times over many years, such that today we can do insanely
large applications in a quite stable environment.
Now that TTY and Proof General support has been finally deleted from the
code-base, I can revisit some old problems in a better way, to make the
system even more stable.
Welcome to Isabelle/HOL (Isabelle2014: August 2014)
poly: gc_mark_phase.cpp:439: virtual void
MTGCProcessMarkPointers::ScanAddressesInObject(PolyObject*,
POLYUNSIGNED): Assertion `baseAddr > (PolyWord*)obj && baseAddr <
((PolyWord*)obj)+length' failed.
See also this thread "Report of Crash of Isabelle 2014"
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2014-December/msg00097.html
Makarius
Last updated: Oct 31 2025 at 01:43 UTC