From 86afcf4f158a8db684800a06796f96c579edc20c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 16 Sep 2019 13:10:25 +0200
Subject: [PATCH] [wp/why3] allow parallel tasks up to -wp-par
---
src/plugins/wp/ProverTask.ml | 9 +++++++--
src/plugins/wp/Why3Provers.ml | 2 ++
src/plugins/wp/Why3Provers.mli | 1 +
3 files changed, 10 insertions(+), 2 deletions(-)
diff --git a/src/plugins/wp/ProverTask.ml b/src/plugins/wp/ProverTask.ml
index e9bb77dc5b5..02390f98b14 100644
--- a/src/plugins/wp/ProverTask.ml
+++ b/src/plugins/wp/ProverTask.ml
@@ -292,9 +292,14 @@ let getprocs = function Some n -> n | None -> Wp_parameters.Procs.get ()
let server ?procs () =
match !server with
| Some s ->
- Task.set_procs s (getprocs procs) ; s
+ let np = getprocs procs in
+ Task.set_procs s np ;
+ Why3Provers.set_procs np ;
+ s
| None ->
- let s = Task.server ~procs:(getprocs procs) () in
+ let np = getprocs procs in
+ let s = Task.server ~procs:np () in
+ Why3Provers.set_procs np ;
Task.on_server_stop s Proof.savescripts ;
server := Some s ; s
diff --git a/src/plugins/wp/Why3Provers.ml b/src/plugins/wp/Why3Provers.ml
index 1bb6c8bd183..7499579fe54 100644
--- a/src/plugins/wp/Why3Provers.ml
+++ b/src/plugins/wp/Why3Provers.ml
@@ -35,6 +35,8 @@ let cfg = lazy
let version = Why3.Config.version
let config () = Lazy.force cfg
+let set_procs = Why3.Controller_itp.set_session_max_tasks
+
let configure =
let todo = ref true in
begin fun () ->
diff --git a/src/plugins/wp/Why3Provers.mli b/src/plugins/wp/Why3Provers.mli
index a68eeb567d8..d08bf2d0337 100644
--- a/src/plugins/wp/Why3Provers.mli
+++ b/src/plugins/wp/Why3Provers.mli
@@ -23,6 +23,7 @@
val version : string
val config : unit -> Why3.Whyconf.config
val configure : unit -> unit
+val set_procs : int -> unit
type t = Why3.Whyconf.prover
--
GitLab