Re: [Why3-club] why3-0.88.0 and CVC4 1.4/1.5

2017-10-23 Thread Claude Marché
Hello, [forwarding to Frama-C list since other users of WP plug-in may help] Le 20/10/2017 à 14:07, Gerlach, Jens a écrit : > A while ago I experimented with why3-0.87.3 and cvc4. > > At that time I reported that version 1.5 of cvc4 performed considerable > worse than version 1.4. > >

Re: [Why3-club] Running multiple provers in parallel on a single task

2017-10-23 Thread Pierre-Yves Strub
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 : > Thank you for your answer. Yes, I was speaking about process ID that

Re: [Why3-club] Running multiple provers in parallel on a single task

2017-10-23 Thread Claude Marché
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,

Re: [Why3-club] Running multiple provers in parallel on a single task

2017-10-23 Thread Johannes Kanig
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

[Why3-club] Running multiple provers in parallel on a single task

2017-10-23 Thread Pierre-Yves Strub
Dear all, 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. This API has now been removed

Re: [Why3-club] Running multiple provers in parallel on a single task

2017-10-23 Thread Claude Marché
Le 23/10/2017 à 13:59, Pierre-Yves Strub a écrit : > 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

Re: [Why3-club] Running multiple provers in parallel on a single task

2017-10-23 Thread Pierre-Yves Strub
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

Re: [Why3-club] Running multiple provers in parallel on a single task

2017-10-23 Thread Pierre-Yves Strub
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