[isabelle-dev] Parallel auto tools

[Jasmin Christian Blanchette]

Hi all,

Starting with change 061b8257ab9f, the "auto" tools (Auto Solve Direct, Auto Quickcheck, Auto Nitpick, Auto Sledgehammer, and Auto Try) are run in parallel rather than sequentially. Their interaction with Proof General is still synchronous, but at least they get more work done during those few seconds they have at their disposal.

The change relies on "Par_List.get_some", i.e. it uses only user-space ML constructs, and Makarius had a look at it already. Nonetheless when I first tried it Auto Sledgehammer kept on creating zombie SPASS processes (fixed in 4b4dfe05b5d7).

Things should be fine now, but should you experience any problems with zombies or threads gone awry, chances are that this change is responsible, and you should let me know before you waste too much time investigating it yourself.

Thanks for your help.

Jasmin