[isabelle-dev] Isabelle2013-2 release

Makarius makarius at sketis.net
Wed Nov 20 22:49:49 CET 2013


We have a problem with Isabelle2013-1 that cannot be ignored.  A changeset 
is included for information.

Are there any side-conditions on the timing of a follow-up Isabelle2013-2, 
e.g. concerning AFP which needs to be updated once more?

I am basically ready to ship a new release within a few days +/-.  To make 
it not too odd, we could wait until the start of December and label it 
"Isabelle2013-2 (December 2013)", following right after "Isabelle2013-1 
(November 2013)".


The problem was introduced by myself early in September, before wrapping 
up for the Isabelle2013-1 release.  These are more than two months without 
anybody noticing.

Are there any other potential problems of Isabelle2013-1 that were not 
reported yet?  (Did anybody test WWW_Find?)

In ancient times the system was much less complex and more people were 
actively involved in the release -- and these people were sharing a few 
adjacent offices and the lunch table.  The situation is quite different 
today.  There is also an increasing cultural problem, because the very 
notion of "stable software release" is getting lost in the younger 
generation. In fact the very term often sounds like an oxymoron now.

(When this is finished I need to look for a stable Linux release for my 
own machine.  Xubuntu greets me with crash report on every login.  Maybe 
the rock-solid Centos will do.)


 	Makarius
-------------- next part --------------
# HG changeset patch
# User wenzelm
# Date 1384981845 -3600
# Node ID db3d3d99c69df03d9f699028e77655596de3aae9
# Parent  75623b4d625103698a6f09e86b51a8e3d3d799af
register actual group of nested worker context -- relevant for insulated cancellation of exec_ids (see also 78693e46a237, e0169f13bd37);
tuned signature;

diff -r 75623b4d6251 -r db3d3d99c69d src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Mon Nov 11 16:40:07 2013 +0100
+++ b/src/Pure/Concurrent/future.ML	Wed Nov 20 22:10:45 2013 +0100
@@ -48,8 +48,7 @@
   val worker_group: unit -> group option
   val the_worker_group: unit -> group
   val worker_subgroup: unit -> group
-  val worker_nest: string -> ('a -> 'b) -> 'a -> 'b
-  val worker_guest: string -> group -> ('a -> 'b) -> 'a -> 'b
+  val worker_context: string -> group -> ('a -> 'b) -> 'a -> 'b
   type 'a future
   val task_of: 'a future -> task
   val peek: 'a future -> 'a Exn.result option
@@ -110,13 +109,8 @@
 
 fun worker_subgroup () = new_group (worker_group ());
 
-fun worker_nest name f x =
-  setmp_worker_task (Task_Queue.new_task (the_worker_group ()) name NONE) f x;
-
-fun worker_guest name group f x =
-  if is_some (worker_task ()) then
-    raise Fail "Already running as worker thread"
-  else setmp_worker_task (Task_Queue.new_task group name NONE) f x;
+fun worker_context name group f x =
+  setmp_worker_task (Task_Queue.new_task group name NONE) f x;
 
 fun worker_joining e =
   (case worker_task () of
diff -r 75623b4d6251 -r db3d3d99c69d src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Mon Nov 11 16:40:07 2013 +0100
+++ b/src/Pure/PIDE/command.ML	Wed Nov 20 22:10:45 2013 +0100
@@ -57,15 +57,17 @@
       (case expr of
         Expr (exec_id, body) =>
           uninterruptible (fn restore_attributes => fn () =>
-            if Execution.running execution_id exec_id [Future.the_worker_group ()] then
-              let
-                val res =
-                  (body
-                    |> restore_attributes
-                    |> Future.worker_nest "Command.memo_exec"
-                    |> Exn.interruptible_capture) ();
-              in SOME ((), Result res) end
-            else SOME ((), expr)) ()
+            let val group = Future.worker_subgroup () in
+              if Execution.running execution_id exec_id [group] then
+                let
+                  val res =
+                    (body
+                      |> restore_attributes
+                      |> Future.worker_context "Command.memo_exec" group
+                      |> Exn.interruptible_capture) ();
+                in SOME ((), Result res) end
+              else SOME ((), expr)
+            end) ()
       | Result _ => SOME ((), expr)))
   |> (fn NONE => error "Conflicting command execution" | _ => ());
 
diff -r 75623b4d6251 -r db3d3d99c69d src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Mon Nov 11 16:40:07 2013 +0100
+++ b/src/Pure/System/isabelle_process.ML	Wed Nov 20 22:10:45 2013 +0100
@@ -159,8 +159,8 @@
     NONE => raise Runtime.TERMINATE
   | SOME line => map (read_chunk channel) (space_explode "," line));
 
-fun worker_guest e =
-  Future.worker_guest "Isabelle_Process.loop" (Future.new_group NONE) e ();
+fun worker_context e =
+  Future.worker_context "Isabelle_Process.loop" (Future.new_group NONE) e ();
 
 in
 
@@ -168,7 +168,7 @@
   let val continue =
     (case read_command channel of
       [] => (Output.error_msg "Isabelle process: no input"; true)
-    | name :: args => (worker_guest (fn () => run_command name args); true))
+    | name :: args => (worker_context (fn () => run_command name args); true))
     handle Runtime.TERMINATE => false
       | exn => (Output.error_msg (ML_Compiler.exn_message exn) handle crash => recover crash; true);
   in


More information about the isabelle-dev mailing list