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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
