[wp] run all provers for smoke tests

src/plugins/wp/ProverTask.ml

@@ -314,18 +314,25 @@ let schedule task =
   Task.spawn server (Task.thread task)
 
 let silent _ = ()
-let spawn ?(monitor=silent) ?pool ~all
+let spawn ?(monitor=silent) ?pool ~all ~smoke
     (jobs : ('a * bool Task.task) list) =
   if jobs <> [] then
     begin
       let step = ref 0 in
       let monitored = ref [] in
-      let canceled = ref false in
+      let finalized = ref false in
       let callback a r =
         if r then
-          begin if not all && not !canceled then
+          begin
+            if smoke then
+              begin
+                finalized := true ;
+                monitor (Some a) ;
+              end
+            else
+            if not all && not !finalized then
               begin
-                canceled := true ;
+                finalized := true ;
                 monitor (Some a) ;
                 List.iter Task.cancel !monitored ;
               end
@@ -333,7 +340,7 @@ let spawn ?(monitor=silent) ?pool ~all
         else
           begin
             decr step ;
-            if not !canceled && !step = 0 then
+            if not !finalized && !step = 0 then
               monitor None ;
           end in
       let pack (a,t) = Task.thread (t >>= Task.call (callback a)) in

src/plugins/wp/ProverTask.mli

@@ -85,7 +85,7 @@ val schedule : 'a Task.task -> unit
 val spawn :
   ?monitor:('a option -> unit) ->
   ?pool:Task.pool ->
-  all:bool ->
+  all:bool -> smoke:bool ->
   ('a * bool Task.task) list -> unit
 
 (** Spawn all the tasks over the server and retain the first 'validated' one.

src/plugins/wp/prover.ml

@@ -112,7 +112,8 @@ let spawn wpo ~delayed
     let process (mode,prover) =
       prove wpo ?config ~mode ?start ?progress ?result prover in
     let all = Wp_parameters.RunAllProvers.get() in
-    ProverTask.spawn ?monitor ?pool ~all
+    let smoke = Wpo.is_smoke_test wpo in
+    ProverTask.spawn ?monitor ?pool ~all ~smoke
       (List.map
          (fun mp ->
             let prover = snd mp in
@@ -124,3 +125,5 @@ let spawn wpo ~delayed
     let thread = Task.thread process in
     let server = ProverTask.server () in
     Task.spawn server ?pool thread
+
+(* -------------------------------------------------------------------------- *)