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.
Actually, I see alt-ergo running, so I'm not sure that this is the issue.
I have hundreds of VCs. The ide seems to become usable again, with all
the blue circles turned green, when there are maybe 6-7 left.
julia
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
