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.
Best regards,
Guillaume
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
