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
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
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
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,
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
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