Isabelle threads should be daemon threads

[dominique-unruh]

trafficstars

When an Isabelle instance has been created (using System.create), several threads are started for communicating with Isabelle. These are all non-daemon threads. This means that when the main program ends, the JVM does not return but waits indefinitely.

The following snippets shows the threads that keep the JVM from exiting:

    import scala.collection.JavaConverters._
    val threadSet = Thread.getAllStackTraces.keySet.asScala
    for (t <- threadSet if !t.isDaemon)
      println(t.getName)

The output is:

standard_error
standard_output
process_manager
command_input
message_output
process_result
main

Only main should be a non-daemon thread.

(Of course, one can always exit via sys.exit, but that puts the burden on the developer to make sure all possible execution paths end with sys.exit.)

[larsrh]

Fair point. System does have a dispose method though, but one would need to remember calling it.

Instead, Simple_Thread.fork (from PIDE) could be patched accordingly.

[dominique-unruh]

For my application, it's OK (since I can call sys.exit and hopefully am catching all relevant exceptions now).

So it's not a priority for me.

But in general, it might not be just about remembering. E.g., in my application, I have one global Isabelle instance (that can be shared because Isabelle is basically stateless). So, no particular part of the application owns the instance. Since it's an interactive command line application, it's not so problematic because there is a clear exit point, and I simply kill everything with sys.exit in the end. But I could imagine differently structured applications that have several threads and should stop when they are all done. (E.g., some parallelized batch processes.)

But, again, I stress that I managed a workaround, so for me it's not a problem. (However, it can be confusing, because one doesn't see why the application doesn't stop. It looks like it is in a deadlock after throwing an exception.)

(Btw: Simple_Thread.fork even has an argument daemon, unfortunately it's called with the default daemon=false from PIDE.)

[larsrh]

Fair enough. PR welcome :wink: