diff options
| -rw-r--r-- | stm/stm.ml | 14 |
1 files changed, 12 insertions, 2 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 4ff163e082..43db6f3f6c 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -907,7 +907,10 @@ module rec ProofTask : sig val build_proof_here : Stateid.t * Stateid.t -> Loc.t -> Stateid.t -> Proof_global.closed_proof_output Future.computation - + + (* If set, only tasks overlapping with this list are processed *) + val set_perspective : Stateid.t list -> unit + end = struct (* {{{ *) let forward_feedback msg = Hooks.(call forward_feedback msg) @@ -946,9 +949,14 @@ end = struct (* {{{ *) let name = ref "proofworker" let extra_env () = !async_proofs_workers_extra_env + let perspective = ref [] + let set_perspective l = perspective := l + let task_match age t = match age, t with - | `Fresh, BuildProof _ -> true + | `Fresh, BuildProof { t_states } -> + not !Flags.async_proofs_full || + List.exists (fun x -> CList.mem_f Stateid.equal x !perspective) t_states | `Old my_states, States l -> List.for_all (fun x -> CList.mem_f Stateid.equal x my_states) l | _ -> false @@ -1239,6 +1247,8 @@ end = struct (* {{{ *) name, max (time1 +. time2) 0.0001,i) 0 l let set_perspective idl = + ProofTask.set_perspective idl; + TaskQueue.broadcast (Option.get !queue); let open Stateid in let open ProofTask in let overlap s1 s2 = |