[isabelle-dev] Interrupt exceptions using the Par_List combinator get_some

[Lukas Bulwahn]

Hello all,


While trying to parallelize different testing approaches under the hood 
of the quickcheck tool in Isabelle, I frequently noticed that Interrupt 
exceptions were thrown.

Inspecting this problem closer, I distilled the following small example 
that shows an unexpected behaviour:

theory Test
imports Main
begin

ML {*
   Par_List.get_some (fn x => if x = 3 then SOME 3 else NONE) [0,1,2,3];
*}

end

bash script:
   for i in $(seq 1 100); do ../../../bin/isabelle-process -e 'use_thy 
"Test"' -q; done

Running this theory on lxbroy10, in 21 of 100 times, it raises an 
Interrupt exception.

Is this a general issue when working with Par_List.get_some?


N.B.: In my scenario, the function that is parallelized is much larger 
(and should take at least 100 ms for its execution, there I could 
observe similar behaviour as well).
Also on my local machine, the exceptions do not occur, so it is related 
to the machine's configuration as well.



Lukas