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 (if
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
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
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.
>
> This
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
> were available up to
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, bu
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 thi
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,
>
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