Dear Pierre-Yves, On 10/23/2017 06:27 PM, Pierre-Yves Strub wrote:
I'm trying to update EasyCrypt from Why3 0.87 to 0.88. Up to now, we were using the Why3 API to run provers on a task that we create programmatically. To start multiple provers in parallel, we were running our home made machinery that was relying on PID.
are you referring to the process ID? Indeed, why3 doesn't necessarily spawn the prover process itself, so doesn't necessarily have access to the pid.
This API has now been removed (if I understand well because running a prover does not necessarily mean forking a new process in Why3 0.88).
From the API documentation, it seems that I could now achieve the same thing using the Strategy API. However, I failed understanding how the API works. Could someone give me some pointers to which modules/functions I should look at?
Were you previously using sessions? If not, you can just replace your pids by the "prover_call" type of call_provers.mli. The call_on_* functions of that file (and the more high-level ones of driver.mli) return immediately, so they are suitable for running provers in parallel.
-- Johannes Kanig, PhD Senior Software Engineer <ka...@adacore.co _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
