Last thing, when a prover returns that a task is valid, I'd like to be able to kill the other ones (I was doing this with a kill(2) syscall before). Would it be possible to have such a thing with a function using call_prover as argument?
2017-10-23 13:59 GMT+02:00 Pierre-Yves Strub <pierre-y...@strub.nu>: > Hi again, > > If found Call_prover.forward_results in the git repository and this is > definitively what I need. This new API is great as it will allow > EasyCrypt to run multiple provers in parallel under Windows > (currently, we are running provers one by one under win32) & will > allow me to remove all this fork/waitpid stuffs in our code base. I > have a few questions/requests : > > - when do you plan to release Why3 with "forward_results" available > --- if I'm right, it is not present in Why3 0.88.0? > - I need to create search trees or hash tables using job IDs as key, > i.e. using prover_call as key. Currently, breaking the abstraction, I > can see that using the polymorphic comparison/hash functions, all will > be fine... but having explicit eq/compare/hash functions for the > prover_call type would allow me not to rely on breaking the Why3 API > abstraction. > > Best. Pierre-Yves. > > > 2017-10-23 13:36 GMT+02:00 Claude Marché <claude.mar...@inria.fr>: >> >> 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 _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
