Hello, Indeed, the modules Driver and Call_provers provide the necessary entry calls for running provers in parallel.
Note this is a parallelism at the level of the OS processes, it is not done using threads. Call_provers.query_call is not the function that starts a prover, but the function to query if a given running prover task is finished or not, that might be the confusion. The function that starts a prover is Driver.prove_task Hope this helps, - Claude Le 20/11/2017 à 21:10, Ziqing Luo a écrit : > Dear Why3 club, > > I'm currently playing around with the Why3 APIs. > > I noticed that there is a non-blocking function for calling provers : > Call_provers.query_call > > Based on my observation, the Call_provers.query_call is not running in > real parallel. i.e. there is only one thread in total is running, the > second prover_call will not start until the first prover_call finishes. > > Is this true or I didn't use it correctly ? Is there anyway to run > different provers in parallel through these APIs (I know the why3ide can > do this) ? > > bests, > Ziqing Luo > University of Delaware > > > > _______________________________________________ > 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
