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

Lukas Bulwahn bulwahn at in.tum.de
Wed Jul 20 16:57:52 CEST 2011

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

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


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.


More information about the isabelle-dev mailing list