Hello, Indeed, the API from Call_provers.mli has changed (yet another not-well-documented Why3 change, sorry about that)
For sure the use of Why3 "strategies" is not what you need. The main change is that for spawning provers as external processes, Why3 does not anymore proceed using a fork, but instead delegates this to another process so-called "why3server". This approach solved at least two issues: first, it is now compatible with Microsoft Windows OS, and second the size of the forked processes is considerably smaller. From the Why3's user side, there is no visible change, except if you are an advanced user using the API directly. It seems to me that, as suggested by Johannes, the use of the prover_call type should abstract away the unix pid. Regarding your request of having a way to call for available answers from multiple provers, the function Call_prover.forward_results should be what you look for. If something is missing for you in this API, we would be glad to complete it for your need. - Claude Le 23/10/2017 à 13:12, Pierre-Yves Strub a écrit : > 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 > -- Claude Marché | tel: +33 1 69 15 66 08 INRIA Saclay - Île-de-France | Université Paris-sud, Bat. 650 | http://www.lri.fr/~marche/ F-91405 ORSAY Cedex | _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
