[isabelle-dev] New Sledgehammer multitheading model

[Jasmin Blanchette]

Dear list,

Sledgehammer has so far followed a very simple multithreading model: If N cores were available, it ran N different provers in parallel for up to 30 s.

There were some drawbacks to this scheme: Most of us have more provers than cores we'd like to run, and we'd also like the stronger provers to be granted more CPU than weaker ones.

I have now (52b37e8a617b) redesigned Sledgehammer's multithreading model to loosen the connection between threads and provers. The so-called greedy schedule I use for invoking provers is based on an ongoing large-scale evaluation of Sledgehammer.

For end users, the main change should be a higher success rate. Apart from that, the main visible difference is that you may now see several proofs coming from the same prover, instead of one proof by prover, as well as proofs coming from more obscure provers that used not to be run by default.

A few options you can play with, with their default values:

   timeout = 30   (in seconds)
   slices = 24 or 48   (depending on whether you have 4 or 8 cores)
   max_proofs = 4   (max number of proofs shown before bailing out)

Thus, by default, provers are called in time slices of 5 s (= timeout * num cores / slices). With the "verbose" options, you can see the individual prover invocations.

I hope you'll find the new behavior more helpful than annoying. Your feedback is welcome.

Cheers,

Jasmin