Mentions légales du service

Skip to content

Allow running provers in parallel during strategy execution

Xavier Denis requested to merge parallel-strategies into master

This MR adds a new syntax to the call step of strategies allowing you to use | to separate multiple provers which will be invoked in parallel.

If a prover finishes before the others in it's group, it will interrupt them, potentially reducing the execution time of long strategies dramatically by avoiding sequential prover steps.

It does not change the default strategies (yet), though I could do that with not much effort.

Merge request reports