Email Gateway (Aug 22 2022 at 12:19): Email Gateway (Aug 22 2022 at 12:19):From: "C. Diekmann" <diekmann@in.tum.de>
Hi,
I'm testing Isabelle2016-RC0_app.tar.gz on Ubuntu 14.04.3 LTS, Unity,
Linux 4.2.0-22-generic x86_64.
I started it in the shell with
./Isabelle2016-RC0/bin/isabelle jedit
After I exited jEdit (clicking the x in the window), the process was
not gone and it was still active in my shell. The prompt did not
return.
ps aux shows the following processes
diekmann 2412 0.0 0.0 18316 3572 pts/16 S+ 18:05 0:00 bash
/home/diekmann/Downloads/Isabelle2016-RC0/lib/Tools/java
-Duser.language=en -Dawt.useSystemAAFontSettings=on
-Dswing.aatext=true -Dapple.laf.useScreenMenuBar=true
-Dapple.awt.application.name=Isabelle -Xms512m -Xmx2560m -Xss8m
-XX:MetaspaceSize=256m isabelle.Main
diekmann 2442 4.0 21.0 6546964 1701868 pts/16 Sl+ 18:05 9:40
/home/diekmann/Downloads/Isabelle2016-RC0/contrib/jdk/x86_64-linux/jre/bin/java
-server -XX:MinHeapFreeRatio=30 -XX:MaxHeapFreeRatio=60
-XX:+UseConcMarkSweepGC -XX:+CMSParallelRemarkEnabled
-Dfile.encoding=UTF-8 -Disabelle.threads=0 -classpath
/home/diekmann/Downloads/Isabelle2016-RC0/lib/classes/Pure.jar:/home/diekmann/Downloads/Isabelle2016-RC0/contrib/jfreechart-1.0.14-1/lib/iText-2.1.5.jar:/home/diekmann/Downloads/Isabelle2016-RC0/contrib/jfreechart-1.0.14-1/lib/jcommon-1.0.18.jar:/home/diekmann/Downloads/Isabelle2016-RC0/contrib/jfreechart-1.0.14-1/lib/jfreechart-1.0.14.jar:/home/diekmann/Downloads/Isabelle2016-RC0/contrib/jortho-1.0-2/jortho.jar:/home/diekmann/Downloads/Isabelle2016-RC0/contrib/scala-2.11.7/lib/akka-actor_2.11-2.3.10.jar:/home/diekmann/Downloads/Isabelle2016-RC0/contrib/scala-2.11.7/lib/config-1.2.1.jar:/home/diekmann/Downloads/Isabelle2016-RC0/contrib/scala-2.11.7/lib/jline-2.12.1.jar:/home/diekmann/Downloads/Isabelle2016-RC0/contrib/scala-2.11.7/lib/scala-actors-2.11.0.jar:/home/diekmann/Downloads/Isabelle2016-RC0/contrib/scala-2.11.7/lib/scala-actors-migration_2.11-1.1.0.jar:/home/diekmann/Downloads/Isabelle2016-RC0/contrib/scala-2.11.7/lib/scala-compiler.jar:/home/diekmann/Downloads/Isabelle2016-RC0/contrib/scala-2.11.7/lib/scala-continuations-library_2.11-1.0.2.jar:/home/diekmann/Downloads/Isabelle2016-RC0/contrib/scala-2.11.7/lib/scala-continuations-plugin_2.11.7-1.0.2.jar:/home/diekmann/Downloads/Isabelle2016-RC0/contrib/scala-2.11.7/lib/scala-library.jar:/home/diekmann/Downloads/Isabelle2016-RC0/contrib/scala-2.11.7/lib/scalap-2.11.7.jar:/home/diekmann/Downloads/Isabelle2016-RC0/contrib/scala-2.11.7/lib/scala-parser-combinators_2.11-1.0.4.jar:/home/diekmann/Downloads/Isabelle2016-RC0/contrib/scala-2.11.7/lib/scala-reflect.jar:/home/diekmann/Downloads/Isabelle2016-RC0/contrib/scala-2.11.7/lib/scala-swing_2.11-1.0.2.jar:/home/diekmann/Downloads/Isabelle2016-RC0/contrib/scala-2.11.7/lib/scala-xml_2.11-1.0.4.jar:/home/diekmann/Downloads/Isabelle2016-RC0/contrib/xz-java-1.2-1/lib/xz.jar:/home/diekmann/Downloads/Isabelle2016-RC0/src/Tools/jEdit/dist/jedit.jar
-Duser.language=en -Dawt.useSystemAAFontSettings=on
-Dswing.aatext=true -Dapple.laf.useScreenMenuBar=true
-Dapple.awt.application.name=Isabelle -Xms512m -Xmx2560m -Xss8m
-XX:MetaspaceSize=256m isabelle.Main
Checking with -H, it seems that 2412 has started 2442.
ctrl+c in the shell kills the isabelle processes.
Steps to reproduce:
1) Load a large theory with many dependencies, let jEdit open the
theories the theory depends on.
2) On my system, the theories had errors (not yet ported for 2016).
3) Change a file on disc, e.g., mv Scratch.thy Scratch.thy2
4) click away the "deleted on disc" info.
5) While Isabelle is still checking proofs (and finding more errors), close it.
Best Regards,
Cornelius
Email Gateway (Aug 22 2022 at 12:25):From: Makarius <makarius@sketis.net>
This sounds like the JVM/AWT shutdown problem, that I've now addressed in
http://isabelle.in.tum.de/repos/isabelle/rev/8bcbf1c93119
I spent more than half of the day experimenting with variations on the
theme. Hopefully this change is sufficient.
Makarius
Email Gateway (Aug 22 2022 at 12:25):From: Lars Hupel <hupel@in.tum.de>
This sounds like the JVM/AWT shutdown problem, that I've now addressed
in http://isabelle.in.tum.de/repos/isabelle/rev/8bcbf1c93119
For the records, I've also experienced shutdown problems in libisabelle.
The main reason is that the threads created by the thread pool are not
flagged to be daemon, although I don't know whether this is intentional
or not. I solve it by setting the daemon flag:
Cheers
Lars
Email Gateway (Aug 22 2022 at 12:25):From: Makarius <makarius@sketis.net>
The situation is even more entangled.
Quite long ago I started making various threads daemons, in order to
increase chances that the JVM terminates, while these threads are still
hanging around.
But this later caused the problem introduced in Isabelle/3ad2b2055ffc
(05-Oct-2015): the daemon thread was sending something to the AWT thread
and waiting for the result; the AWT thread was already terminated, because
it only waits for non-daemon threads before shutting itself down; so the
wait of the daemon ended up as deadlock.
Today I first tried to make the daemon thread a non-daemon, but got
entangled elesewhere, for unknown reasons.
Then I just gave up the ambition to be ultra-smart in the inter-thread
ping-pong. So in 8bcbf1c93119 we are back to a situation where a daemon
thread sends asynchronously a task on the queue of the AWT thread, without
waiting for a result. It means that the whole task stays on the AWT
thread, when it actually happens -- causing several milliseconds of
potential GUI lock-up.
Makarius
Email Gateway (Aug 22 2022 at 12:26):From: Makarius <makarius@sketis.net>
I've picked up this change as well:
http://isabelle.in.tum.de/repos/isabelle/rev/6dbeafce6318
This means the trend to have service threads as daemons is increased. It
also means that synchronous context switch into the AWT thread needs even
more care as usual. I will double-check all remaining uses of
GUI_Thread.now.
Makarius
Last updated: Apr 20 2024 at 08:16 UTC