Re: [isabelle] Isabelle2014-RC0 segfault / sledgehammer raises exception DUP

On Thu, 24 Jul 2014, Jasmin Christian Blanchette wrote:

I can reproduce the problem with the following (array-free!) theory:

   theory Scratch
   imports Main

   ML {*
   fun launch_thread timeout task =
       val birth_time = ()
       val death_time = Time.+ (birth_time, timeout)
       val desc = ("", "")
       Async_Manager.thread "" birth_time death_time desc task

   ML {*
   launch_thread (seconds 10.0) (fn _ => error "FOO")


In short: Any uncaught exception raised from an old-style "Async_Manager" worker thread eventually leads to a segfault.

The problem can be pushed further down to Runtime.thread, which is marked as "Proof General legacy", but that is not the problem here.

For the moment, the included changeset should prevent that particular crash, but I first need to understand what is really going on.

BTW, the other hard crash with Isabelle2014-RC0 PIDE interaction under heavy load and many auxiliary files is already sorted out: it is a failure of the ML/C foreign language interface and our SHA1.digest that is based on it. (That *is* one of these array algorithms.)

# HG changeset patch
# User wenzelm
# Date 1406217846 -7200
# Node ID 88b52244574df91b0f7d0e6d876176eedb7425f9
# Parent  4b247a7586c92324bf4746a3ad760822129f2135
adhoc workaround to avoid hard crash after ML exception;

diff -r 4b247a7586c9 -r 88b52244574d src/Pure/Isar/runtime.ML
--- a/src/Pure/Isar/runtime.ML	Thu Jul 24 17:58:29 2014 +0200
+++ b/src/Pure/Isar/runtime.ML	Thu Jul 24 18:04:06 2014 +0200
@@ -153,11 +153,7 @@
     if Exn.is_interrupt exn then reraise exn
-        val opt_ctxt =
-          (case Context.thread_data () of
-            NONE => NONE
-          | SOME context => try Context.proof_of context);
-        val _ = output_exn (exn_context opt_ctxt exn);
+        val _ = output_exn (exn_context NONE exn);
       in raise TOPLEVEL_ERROR end;
 fun toplevel_program body =

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.