[isabelle-dev] New Sledgehammer multitheading model

[Jasmin Blanchette]

Hi Tobias,

> That is because you invoke the same prover with different parameters?

Exactly. Different number of lemmas (e.g., 128 or 1024), different sources for these lemmas (MaSh, MePo, MeSh), and different options to the provers themselves.

Sledgehammer already had such "time slicing" on a per-prover basis -- e.g. it would call SPASS first with set-of-support then without, within one same thread. But with the new model things are more anarchic.

Jasmin