Sorry, my sentence is unclear: We're not using sessions but are already using Driver.prove_task which returns a Call_provers.prover_call (as the call_on_*).
2017-10-23 13:12 GMT+02:00 Pierre-Yves Strub <pierre-y...@strub.nu>: > Thank you for your answer. Yes, I was speaking about process ID that > were available up to Why 0.87. We're not using sessions and > Driver.prove_task which returns a Call_provers.prover_call (as the > call_on_*). The problem is that with the new API, I don't have any way > to wait for multiple provers (in a non-active way, i.e. without > spamming query_call). I'm ok to move to any API as long as I can call > multiple provers on a task and wait until on prover succeeds. > > Best. Pierre-Yves. > > 2017-10-23 11:47 GMT+02:00 Johannes Kanig <ka...@adacore.com>: >> 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 _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
