On Sat, 20 Apr 2019, Guillaume Melquiond wrote:
> Le 19/04/2019 à 13:41, Julia Lawall a écrit :
>
> >> I'm not sure how to help, but I wonder: how many provers you asked Why3
> >> to run in parallel? I suggest you should not use 48, because you will
> >> have no remaining cores for the main Why3 process, and other processes
> >> of your system.
> >
> > I asked for 47.
> >
> > But even if there are only eg 10 things to prove, I still see a
> > smaller but noticible delay.
>
> Keep in mind that Why3 is inherently mono-core. So, Why3 will be
> unusable until the 10 corresponding proof obligations have been
> generated and sent to external provers.
>
> More generally, the more cores you computer has, the more proof
> obligations Why3 needs to generate to feed all the external provers, the
> less usable the user interface becomes.
I looked around a bit. In controller_itp.ml there is a function called
run_timeout_handler. I printed the difference between the time when this
function is called and when timeout_handler runs. run_timeout_handler is
only called once in my test. timeout_handler is first run after 0.4
seconds. The next run is after 25 more seconds, when it calls
read_answers. The delays after that are 6-7 seconds. Is this expected?
julia
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
