[isabelle-dev] New Sledgehammer multitheading model

Jasmin Blanchette j.c.blanchette at vu.nl
Tue Feb 1 16:52:43 CET 2022


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



More information about the isabelle-dev mailing list